theorem add_S_1: \forall p,q,r. add p q r \to add (S p) q (S r).
intros 2. elim q; clear q;
theorem add_S_1: \forall p,q,r. add p q r \to add (S p) q (S r).
intros 2. elim q; clear q;
theorem add_sym: \forall p,q,r. add p q r \to add q p r.
intros 2. elim q; clear q;
theorem add_sym: \forall p,q,r. add p q r \to add q p r.
intros 2. elim q; clear q;
\forall q2,r2. add r1 q2 r2 \to
\exists q. add q1 q2 q \land add p q r2.
intros 2; elim q1; clear q1; intros;
\forall q2,r2. add r1 q2 r2 \to
\exists q. add q1 q2 q \land add p q r2.
intros 2; elim q1; clear q1; intros;
\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;
\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;
theorem add_conf: \forall p,q,r1. add p q r1 \to
\forall r2. add p q r2 \to r1 = r2.
intros 2. elim q; clear q; intros;
theorem add_conf: \forall p,q,r1. add p q r1 \to
\forall r2. add p q r2 \to r1 = r2.
intros 2. elim q; clear q; intros;