proposition: Lemma codeSysPfCorrect : forall f : fol.Formula L, folProof.SysPrf L U f -> SysPrf T (substF codeSysPf 0 (natToTerm (codeFormula f))).
proof: Proof. intros f [x [x0 H]]; unfold codeSysPf; rewrite (subFormulaExist LNN). induction (eq_nat_dec 1 0) as [a | b]. - discriminate a. - induction (In_dec eq_nat_dec 1 (freeVarT (natToTerm (codeFormula f)))) as [a | b0]. + elim (closedNatToTerm _ _ a). + apply existI with (natToTerm (codePrf _ _ x0)). now apply codeSysPrfCorrect1. Qed.
imports: Coq(Ensembles) Coq(List) hydras.Ackermann(checkPrf) hydras.Ackermann(code) hydras.Ackermann(Languages) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folLogic3) hydras.Ackermann(folReplace) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(primRec) Coq(Arith Lia) hydras.Ackermann(PA) hydras.Ackermann(NNtheory) hydras.Ackermann(codeList) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) hydras.Ackermann(cPair) hydras.Ackermann(wellFormed) hydras.Ackermann(prLogic) hydras(Compat815)