case succ i h_ind =>
  dsimp [getBit]; 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) (succ i) = f (getBit m (succ i)) (getBit n (succ i))
no goals