cases hm
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : m = 0
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ bitwise f 0 n % 2 = if f (decide (0 % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0