-theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to
- \exists s. p = succ s \land (s + q == r) \lor
- q = succ s \land p + s == r.
- intros. inversion H; clear H; intros;
- [ subst
- | clear H1. destruct H3. clear H3. subst.
- ]; auto depth = 4.
+theorem nplus_inv_succ_3: ∀p,q,r. p ⊕ q ≍ succ r →
+ ∃s. p = succ s ∧ s ⊕ q ≍ r ∨
+ q = succ s ∧ p ⊕ s ≍ r.
+ intros; inversion H; clear H; intros; destruct;
+ autobatch depth = 4.