Theorem: bitvec_AddSub_1556 (Eval/bitvec_AddSub_1556.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