case pos hm =>
  cases hm; simp
  unfold bitwise; simp
  cases hft : f false true
  case false =>
    have : ∀ b, f false b = false := by intro b; cases b <;> assumption
    simp [this]
  case true =>
    have : ∀ b, f false b = b := by intro b; cases b <;> assumption
    simp [this]
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
no goals