proposition: Lemma eqPlus (T : System) (a b c d : Term): SysPrf T (a = b)%nt -> SysPrf T (c = d)%nt -> SysPrf T (a + c = b + d)%nt.
proof: Proof. intros H H0; unfold Plus; apply (equalFunction LNT). simpl in |- *. destruct (consTerms LNT 1 (Tcons a (Tcons c (Tnil))))as [(a0,b0) p]. simpl; destruct (consTerms LNT 1 (Tcons b (Tcons d (Tnil)))) as [(a1,b1) p0]. simpl in |- *. destruct (consTerms LNT 0 b0) as [(a2,b2) p1]. simpl in |- *. destruct (consTerms LNT 0 b1) as [(a3,b3) p2]. simpl in |- *; repeat split. - simpl in p. inversion p. simpl in p0. inversion p0. apply H. - simpl in p. inversion p. rewrite <- p1 in H3. simpl in H3. inversion H3. simpl in p0. inversion p0. rewrite <- p2 in H7. inversion H7. apply H0. Qed.
imports: Coq(Arith Ensembles List) hydras.Ackermann(Languages folProof folProp folLogic3)