proposition: Lemma codeTermsInj : forall (n : nat) (ts ss : Terms n), codeTerms n ts = codeTerms n ss -> ts = ss.
proof: Proof. intros n ts; induction ts as [| n t ts Hrects]. - intros ss H; now rewrite <- (nilTerms L ss). - intros ss H. destruct (consTerms L n ss) as [(a,b) p]. simpl in p; rewrite <- p in H |- *. rewrite (Hrects b). + rewrite (codeTermInj t a). * reflexivity. * eapply cPairInj1. apply eq_add_S, H. + eapply cPairInj2. apply eq_add_S, H. Qed.
imports: Coq(Arith) hydras.Ackermann(fol folProof cPair)