Bool.sizeOf_eq_one

theorem Bool.sizeOf_eq_one : ∀ (b : Bool), sizeOf b = 1

This theorem states that the size of any Boolean value is 1. In other words, for every Boolean value 'b', when we calculate its size using the 'sizeOf' function, we will always get the result as 1.

More concisely: For all Boolean values 'b' in Lean, the size is 1: size Lean.Bool b = 1.