proposition: Lemma eqPlus (T : System) (a b c d : Term): SysPrf T (a = b)%fol -> SysPrf T (c = d)%fol -> SysPrf T (a + c = b + d)%fol.
proof: Proof. intros H H0; unfold Plus; apply (equalFunction); simpl. destruct (consTerms LNN 1 (Tcons a (Tcons c (Tnil)))) as [(a0, b0) p]. simpl; destruct (consTerms LNN 1 (Tcons b (Tcons d (Tnil)))) as [(a1, b1) p0]. simpl; destruct (consTerms LNN 0 b0) as [(a2, b2) p1]. simpl; destruct (consTerms LNN 0 b1) as [(a3,b3) p2]. simpl; repeat split. - simpl in p; inversion p /r; intros H2 H3. simpl in p0; inversion p0 /r; intros H4 H5. apply H. - simpl in p; inversion p /r; intros H2 H3. rewrite <- p1 in H3. simpl in H3; inversion H3 /r; intros H4 H5. simpl in p0; inversion p0 /r; intros H6 H7. rewrite <- p2 in H7. inversion H7; apply H0. Qed.
imports: Coq(Arith Ensembles List) LibHyps(LibHyps) hydras(MoreLibHyps NewNotations)