intro i
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n % 2 ^ k) i = getBit (bitwise f (m % 2 ^ k) (n % 2 ^ k)) i
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n % 2 ^ k) i = getBit (bitwise f (m % 2 ^ k) (n % 2 ^ k)) i