cases m.eq_zero_of_lt_one hmk
f : Bool → Bool → Bool
m n : Nat
hmk : m < 2 ^ zero
hnk : n < 2 ^ zero
⊢ bitwise f m n < 2 ^ zero
case refl
f : Bool → Bool → Bool
n : Nat
hnk : n < 2 ^ zero
hmk : 0 < 2 ^ zero
⊢ bitwise f 0 n < 2 ^ zero