case pos hm =>
  cases hm; unfold bitwise; simp
  cases hfft : f false true
  case false =>
    have : ∀ b, f false b = false := λ b => by cases b; exact f_stable; exact hfft
    simp [this]
  case true =>
    have : ∀ b, f false b = b := λ b => by cases b; exact f_stable; exact hfft
    simp [this]
    apply (n.mod_two_eq_zero_or_one).elim <;> intro h <;> simp [h]
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : m = 0
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
no goals