Theorem: bitvec_290__292 (Eval/bitvec_290__292.lean)

State before:
⊢ ∀ (Y Op1 : BitVec 64), 1#64 <<< Y * Op1 = Op1 <<< Y
Tactic:
intros
State after:
Y✝ Op1✝ : BitVec 64
⊢ 1#64 <<< Y✝ * Op1✝ = Op1✝ <<< Y✝

State before:
Y✝ Op1✝ : BitVec 64
⊢ 1#64 <<< Y✝ * Op1✝ = Op1✝ <<< Y✝
Tactic:
bv_decide
State after:
no goals