Theorem: bitvec_AndOrXor_144 (Eval/bitvec_AndOrXor_144.lean)

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

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