simp [this]
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
this : ∀ (b : Bool), f false b = false
⊢ (if false = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0
no goals