cases hftf : f true false
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
⊢ (if f true false = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0
case refl.false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ (if false = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0

case refl.true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ (if true = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0