apply bitext
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ bitwise f m n >>> k = bitwise f (m >>> k) (n >>> k)
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