by_cases m = 0
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
case pos
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
h✝ : m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)

case neg
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
h✝ : ¬m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)