Theorem: bitvec_160 (Eval/bitvec_160.lean)

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

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