Theorem: bitvec_InstCombineShift__724 (Eval/bitvec_InstCombineShift__724.lean)

State before:
⊢ ∀ (A C2 C1 : BitVec 31), C1 <<< A <<< C2 = C1 <<< C2 <<< A
Tactic:
intros
State after:
A✝ C2✝ C1✝ : BitVec 31
⊢ C1✝ <<< A✝ <<< C2✝ = C1✝ <<< C2✝ <<< A✝

State before:
A✝ C2✝ C1✝ : BitVec 31
⊢ C1✝ <<< A✝ <<< C2✝ = C1✝ <<< C2✝ <<< A✝
Tactic:
bv_decide
State after:
no goals