proposition: Lemma codeFormulaInj : forall f g : Formula, codeFormula f = codeFormula g -> f = g.
proof: Proof. intro f; induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; intros; [ destruct g as [t1 t2| r t1| f f0| f| n f] | destruct g as [t0 t1| r0 t0| f f0| f| n f] | destruct g as [t t0| r t| f f2| f| n f] | destruct g as [t t0| r t| f0 f1| f0| n f0] | destruct g as [t t0| r t| f0 f1| f0| n0 f0] ]; (simpl in H; try match goal with | h:(cPair ?X1 ?X2 = cPair ?X3 ?X4) |- _ => assert False by ( cut (X1 = X3); [ discriminate | eapply cPairInj1; apply h ]); contradiction end). - rewrite (codeTermInj t t1). + rewrite (codeTermInj t0 t2). * reflexivity. * eapply cPairInj2. eapply cPairInj2. apply H. + eapply cPairInj1. eapply cPairInj2. apply H. - assert (r = r0). { eapply codeRInj. apply cl. do 4 apply eq_add_S. eapply cPairInj1. apply H. } cut (cPair (S (S (S (S (codeR cl r))))) (codeTerms (arityR L r) t) = cPair (S (S (S (S (codeR cl r0))))) (codeTerms (arityR L r0) t0)). + generalize t0; rewrite <- H0; clear H0 H t0. intros t0 H; rewrite (codeTermsInj _ t t0). * reflexivity. * eapply cPairInj2; apply H. + apply H. - rewrite (Hrecf1 f). + rewrite (Hrecf0 f2). * reflexivity. * eapply cPairInj2. eapply cPairInj2. apply H. + eapply cPairInj1. eapply cPairInj2; apply H. - rewrite (Hrecf f0). reflexivity. eapply cPairInj2. apply H. - rewrite (Hrecf f0). + replace n0 with n. * reflexivity. * eapply cPairInj1. eapply cPairInj2. apply H. + eapply cPairInj2. eapply cPairInj2. apply H. Qed.
imports: Coq(Arith) hydras.Ackermann(fol folProof cPair)