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