proposition: Lemma expressT'1 : forall f : Formula, mem _ T f -> folProof.SysPrf LNN T' (substF (LNT2LNN_formula repT) v0 (natToTermLNN (codeFormula f))).
proof: Proof. intros f H; rewrite <- (LNT2LNN_natToTerm (codeFormula f)), <- LNT2LNN_subFormula; now apply Tprf2T'prf, expressT1. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith Lia) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folReplace) hydras.Ackermann(folLogic3) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) hydras.Ackermann(NNtheory) hydras.Ackermann(NN2PA) Goedel(fixPoint) Goedel(codeSysPrf) hydras.Ackermann(PAtheory) hydras.Ackermann(code) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) hydras(Compat815)