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 >>> k) i = getBit (bitwise f (m >>> k) (n >>> k)) i
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n >>> k) i = getBit (bitwise f (m >>> k) (n >>> k)) i