case pos hn =>
  cases hn; simp
  cases hftf : f true false
  case true =>
    have : ∀ b, f b false = b := λ b => by cases b; exact f_stable; exact hftf
    simp [this]
    apply m.mod_two_eq_zero_or_one.elim <;> intro h <;> simp [h]
  case false =>
    have : ∀ b, f b false = false := λ b => by cases b; exact f_stable; exact hftf
    simp [this]
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : n = 0
⊢ (if n = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
no goals