Theorem: bitvec_AndOrXor_135 (Eval/bitvec_AndOrXor_135.lean)

State before:
⊢ ∀ (X C1 C2 : BitVec 64), (X ^^^ C1) &&& C2 = X &&& C2 ^^^ C1 &&& C2
Tactic:
intros
State after:
X✝ C1✝ C2✝ : BitVec 64
⊢ (X✝ ^^^ C1✝) &&& C2✝ = X✝ &&& C2✝ ^^^ C1✝ &&& C2✝

State before:
X✝ C1✝ C2✝ : BitVec 64
⊢ (X✝ ^^^ C1✝) &&& C2✝ = X✝ &&& C2✝ ^^^ C1✝ &&& C2✝
Tactic:
bv_decide
State after:
no goals