qed.
theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to
\forall p2,r2. add p2 r1 r2 \to
\exists p. add p1 p2 p \land add p q r2.
intros 2; elim q; clear q; intros;
qed.
theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to
\forall p2,r2. add p2 r1 r2 \to
\exists p. add p1 p2 p \land add p q r2.
intros 2; elim q; clear q; intros;