Theorem: bitvec_InstCombineShift__497 (Eval/bitvec_InstCombineShift__497.lean)

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

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