case zero =>
  cases m.eq_zero_of_lt_one hmk; cases n.eq_zero_of_lt_one hnk
  unfold bitwise; simp
f : Bool → Bool → Bool
m n : Nat
hmk : m < 2 ^ zero
hnk : n < 2 ^ zero
⊢ bitwise f m n < 2 ^ zero
no goals