case pos hm =>
  cases hm
  unfold bitwise; simp
  cases f false true <;> simp
  . exact Nat.pos_pow_of_pos k.succ (Nat.zero_lt_succ 1)
  . exact hnk
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : m = 0
⊢ bitwise f m n < 2 ^ succ k
no goals