proposition: Lemma eqSucc (T : System) (a b : Term): SysPrf T (a = b)%nt -> SysPrf T (Succ a = Succ b)%nt.
proof: Proof. intros H; unfold Succ in |- *; apply (equalFunction LNT). simpl in |- *. destruct (consTerms LNT 0 (Tcons a (Tnil))) as [(a0,b0) p]. simpl in |- *; destruct (consTerms LNT 0 (Tcons b (Tnil))) as [(a1,b1) p0]. simpl in |- *; repeat split. - simpl in p; inversion p /r; intros ? ?. simpl in p0; inversion p0; apply H. Qed.
imports: Coq(Arith Ensembles List) hydras.Ackermann(Languages folProof folProp folLogic3)