Theorem: bitvec_InstCombineShift__239 (Eval/bitvec_InstCombineShift__239.lean)

State before:
⊢ ∀ (X C : BitVec 64), X <<< C >>> C = X &&& (-1) >>> C
Tactic:
intros
State after:
X✝ C✝ : BitVec 64
⊢ X✝ <<< C✝ >>> C✝ = X✝ &&& (-1) >>> C✝

State before:
X✝ C✝ : BitVec 64
⊢ X✝ <<< C✝ >>> C✝ = X✝ &&& (-1) >>> C✝
Tactic:
bv_decide
State after:
no goals