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