cases htf : f true false
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
⊢ getBit (if f true false = true then m else 0) 0 = f (getBit m 0) false
case refl.false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
⊢ getBit (if false = true then m else 0) 0 = f (getBit m 0) false

case refl.true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
⊢ getBit (if true = true then m else 0) 0 = f (getBit m 0) false