-theorem nplus_trans_1: \forall p,q1,r1. NPlus p q1 r1 \to
- \forall q2,r2. NPlus r1 q2 r2 \to
- \exists q. NPlus q1 q2 q \land NPlus p q r2.
+theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
+ \forall q2,r2. (r1 + q2 == r2) \to
+ \exists q. (q1 + q2 == q) \land p + q == r2.