induction i generalizing m n
f : Bool → Bool → Bool
f_stable : f false false = false
m n i : Nat
⊢ getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
case zero
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 succ
f : Bool → Bool → Bool
f_stable : f false false = false
n✝ : Nat
n_ih✝ : ∀ (m n : Nat), getBit (bitwise f m n) n✝ = f (getBit m n✝) (getBit n n✝)
m n : Nat
⊢ getBit (bitwise f m n) (succ n✝) = f (getBit m (succ n✝)) (getBit n (succ n✝))