Theorem: bitvec_AddSub_1539 (Eval/bitvec_AddSub_1539.lean)

State before:
⊢ ∀ (a x : BitVec 64), x - (0 - a) = x + a
Tactic:
intros
State after:
a✝ x✝ : BitVec 64
⊢ x✝ - (0 - a✝) = x✝ + a✝

State before:
a✝ x✝ : BitVec 64
⊢ x✝ - (0 - a✝) = x✝ + a✝
Tactic:
bv_decide
State after:
no goals