f : Bool → Bool → Bool
⊢ (bif f false true then 0 else 0) = 0
f : Bool → Bool → Bool
⊢ bitwise' f 0 0 = 0
rw [bitwise'_zero_left]
no goals
f : Bool → Bool → Bool
⊢ (bif f false true then 0 else 0) = 0
cases f false true <;> rfl