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