rw [bitwise_div_two, h_ind]
f : Bool → Bool → Bool
f_stable : f false false = false
i : Nat
h_ind : ∀ (m n : Nat), getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
m n : Nat
⊢ getBit (bitwise f m n / 2) i = f (getBit (m / 2) i) (getBit (n / 2) i)
no goals