cases b
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
b : Bool
⊢ f b false = b
case false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ f true false = true