rw [if_pos (Eq.refl 0)]
case refl
f : Bool → Bool → Bool
⊢ (if f true false = true then 0 else 0) = if 0 = 0 then 0 else if f true false = true then 0 else 0
case refl
f : Bool → Bool → Bool
⊢ (if f true false = true then 0 else 0) = 0