Theorem: bitvec_AddSub_1574 (Eval/bitvec_AddSub_1574.lean)

State before:
⊢ ∀ (X C C2 : BitVec 64), C - (X + C2) = C - C2 - X
Tactic:
intros
State after:
X✝ C✝ C2✝ : BitVec 64
⊢ C✝ - (X✝ + C2✝) = C✝ - C2✝ - X✝

State before:
X✝ C✝ C2✝ : BitVec 64
⊢ C✝ - (X✝ + C2✝) = C✝ - C2✝ - X✝
Tactic:
bv_decide
State after:
no goals