qed.
theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to
\forall p2. (p2 + q == r) \to p2 = p1.
intros 4. elim H; clear H q r;
qed.
theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to
\forall p2. (p2 + q == r) \to p2 = p1.
intros 4. elim H; clear H q r;