Theorem: bitvec_283 (Eval/bitvec_283.lean)

State before:
⊢ ∀ (Y X : BitVec 1), X * Y = X &&& Y
Tactic:
intros
State after:
Y✝ X✝ : BitVec 1
⊢ X✝ * Y✝ = X✝ &&& Y✝

State before:
Y✝ X✝ : BitVec 1
⊢ X✝ * Y✝ = X✝ &&& Y✝
Tactic:
bv_decide
State after:
no goals