proposition: Lemma eqSucc (T : System) (a b : Term): SysPrf T (a = b)%fol -> SysPrf T (Succ a = Succ b)%fol.
proof: Proof. intro H; unfold Succ; apply (equalFunction LNN). simpl; destruct (consTerms LNN 0 (Tcons a (Tnil))) as [(a0, b0) p]. simpl; destruct (consTerms LNN 0 (Tcons b (Tnil))) as [(a1, b1) p0]. simpl; repeat split. simpl in p. inversion p /r; intros H1 H2; simpl in p0. inversion p0; apply H. Qed.
imports: Coq(Arith Ensembles List) LibHyps(LibHyps) hydras(MoreLibHyps NewNotations)