proposition: Lemma codeTermInj : forall t s : Term, codeTerm t = codeTerm s -> t = s.
proof: Proof. intro t; elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => forall ss : Terms n, codeTerms n ts = codeTerms n ss -> ts = ss). - intros n s H; destruct s. + simpl in H; apply cPairInj2 in H; now subst. + simpl in H. assert (H0: 0 = S (codeF cl f)) by (eapply cPairInj1; apply H). discriminate H0. - intros f t0 H s H0; destruct s. + simpl in H0. assert (H1: S (codeF cl f) = 0) by (eapply cPairInj1; apply H0). discriminate H1. + simpl in H0; assert (H1: f = f0). { eapply codeFInj. apply cl. apply eq_add_S; eapply cPairInj1; apply H0. } cut (cPair (S (codeF cl f)) (codeTerms (arityF L f) t0) = cPair (S (codeF cl f0)) (codeTerms (arityF L f0) t1)). * generalize t1; rewrite <- H1; clear H1 H0 t1. intros t1 H0; rewrite (H t1). -- reflexivity. -- eapply cPairInj2. apply H0. * apply H0. - intros ss H; rewrite <- nilTerms; reflexivity. - intros n t0 H t1 H0 ss H1; induction (consTerms L n ss). destruct x as (a, b); simpl in p; rewrite <- p. rewrite <- p in H1; simpl in H1; rewrite (H a). + rewrite (H0 b). * reflexivity. * eapply cPairInj2; apply eq_add_S, H1. + eapply cPairInj1. apply eq_add_S, H1. Qed.
imports: Coq(Arith) hydras.Ackermann(fol folProof cPair)