-theorem nplus_ass: \forall p1, p2, r1. (p1 + p2 == r1) \to
- \forall p3, s1. (r1 + p3 == s1) \to
- \forall r3. (p2 + p3 == r3) \to
- \forall s3. (p1 + r3 == s3) \to s1 = s3.
- intros 4. elim H; clear H p2 r1;
+theorem nplus_ass: ∀p1, p2, r1. p1 ⊕ p2 ≍ r1 → ∀p3, s1. r1 ⊕ p3 ≍ s1 →
+ ∀r3. p2 ⊕ p3 ≍ r3 → ∀s3. p1 ⊕ r3 ≍ s3 → s1 = s3.
+ intros 4; elim H; clear H p2 r1;