proposition: Lemma codePrfInjAxm : forall (a b : Formula) (A B : Formulas) (p : Prf A a) (q : Prf B b), codePrf A a p = codePrf B b q -> A = B.
proof: Proof. intros a b A B p; generalize B b; clear B b. induction p as [A| Axm1 Axm2 A B p1 Hrecp1 p0 Hrecp0| Axm A v n p Hrecp| A B| A B C| A B| A v t| A v n| A B v| | | | R| f]; intros; [ destruct q as [A0| Axm1 Axm2 A0 B p p0| Axm A0 v n p| A0 B| A0 B C| A0 B| A0 v t| A0 v n| A0 B v| | | | R| f] | destruct q as [A0| Axm0 Axm3 A0 B0 p p2| Axm A0 v n p| A0 B0| A0 B0 C| A0 B0| A0 v t| A0 v n| A0 B0 v| | | | R| f] | destruct q as [A0| Axm1 Axm2 A0 B p0 p1| Axm0 A0 v0 n0 p0| A0 B| A0 B C| A0 B| A0 v0 t| A0 v0 n0| A0 B v0| | | | R| f] | destruct q as [A0| Axm1 Axm2 A0 B0 p p0| Axm A0 v n p| A0 B0| A0 B0 C| A0 B0| A0 v t| A0 v n| A0 B0 v| | | | R| f] | destruct q as [A0| Axm1 Axm2 A0 B0 p p0| Axm A0 v n p| A0 B0| A0 B0 C0| A0 B0| A0 v t| A0 v n| A0 B0 v| | | | R| f] | destruct q as [A0| Axm1 Axm2 A0 B0 p p0| Axm A0 v n p| A0 B0| A0 B0 C| A0 B0| A0 v t| A0 v n| A0 B0 v| | | | R| f] | destruct q as [A0| Axm1 Axm2 A0 B p p0| Axm A0 v0 n p| A0 B| A0 B C| A0 B| A0 v0 t0| A0 v0 n| A0 B v0| | | | R| f] | destruct q as [A0| Axm1 Axm2 A0 B p p0| Axm A0 v0 n0 p| A0 B| A0 B C| A0 B| A0 v0 t| A0 v0 n0| A0 B v0| | | | R| f] | destruct q as [A0| Axm1 Axm2 A0 B0 p p0| Axm A0 v0 n p| A0 B0| A0 B0 C| A0 B0| A0 v0 t| A0 v0 n| A0 B0 v0| | | | R| f] | destruct q as [A| Axm1 Axm2 A B p p0| Axm A v n p| A B| A B C| A B| A v t| A v n| A B v| | | | R| f] | destruct q as [A| Axm1 Axm2 A B p p0| Axm A v n p| A B| A B C| A B| A v t| A v n| A B v| | | | R| f] | destruct q as [A| Axm1 Axm2 A B p p0| Axm A v n p| A B| A B C| A B| A v t| A v n| A B v| | | | R| f] | destruct q as [A| Axm1 Axm2 A B p p0| Axm A v n p| A B| A B C| A B| A v t| A v n| A B v| | | | R0| f] | destruct q as [A| Axm1 Axm2 A B p p0| Axm A v n p| A B| A B C| A B| A v t| A v n| A B v| | | | R| 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); try reflexivity. - replace A0 with A. + reflexivity. + apply codeFormulaInj; eapply cPairInj2, H. - replace Axm0 with Axm1. + replace Axm3 with Axm2. * reflexivity. * eapply Hrecp0 with A0 p2. do 3 eapply cPairInj2. apply H. + eapply Hrecp1 with (impH A0 B0) p. eapply cPairInj2. eapply cPairInj1. eapply cPairInj2. apply H. - eapply Hrecp with A0 p0. do 3 eapply cPairInj2. apply H. Qed.
imports: Coq(Arith) hydras.Ackermann(fol folProof cPair)