Theorem: bitvec_InstCombineShift__351 (Eval/bitvec_InstCombineShift__351.lean)

State before:
⊢ ∀ (X C1 C2 : BitVec 7), (X * C1) <<< C2 = X * C1 <<< C2
Tactic:
intros
State after:
X✝ C1✝ C2✝ : BitVec 7
⊢ (X✝ * C1✝) <<< C2✝ = X✝ * C1✝ <<< C2✝

State before:
X✝ C1✝ C2✝ : BitVec 7
⊢ (X✝ * C1✝) <<< C2✝ = X✝ * C1✝ <<< C2✝
Tactic:
bv_decide
State after:
no goals