Theorem: bitvec_AddSub_1156 (Eval/bitvec_AddSub_1156.lean)

State before:
⊢ ∀ (b : BitVec 64), b + b = b <<< 1
Tactic:
intros
State after:
b✝ : BitVec 64
⊢ b✝ + b✝ = b✝ <<< 1

State before:
b✝ : BitVec 64
⊢ b✝ + b✝ = b✝ <<< 1
Tactic:
bv_decide
State after:
no goals