cases hn
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ bitwise f m 0 / 2 = bitwise f (m / 2) (0 / 2)