cases hn
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
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