Theorem: bitvec_InstCombineShift__279 (Eval/bitvec_InstCombineShift__279.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