case pos hn =>
  cases hn; rw [if_pos (Eq.refl 0)]
  by_cases f true false <;> simp
f : Bool → Bool → Bool
n : Nat
hn : n = 0
⊢ (if f true false = true then n else 0) = if n = 0 then 0 else if f true false = true then n else 0
no goals