by_cases n = 0
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (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 pos
f : Bool → Bool → Bool
n : Nat
h✝ : 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 neg
f : Bool → Bool → Bool
n : Nat
h✝ : ¬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