cases hft : f false true
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (if f false true = true then n else 0) 0 = f false (getBit n 0)
case refl.false
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
⊢ getBit (if false = true then n else 0) 0 = f false (getBit n 0)

case refl.true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
⊢ getBit (if true = true then n else 0) 0 = f false (getBit n 0)