fact: Hypothesis expressT2 : forall f : Formula, ~ mem _ T f -> SysPrf T (notH (substF repT v0 (natToTerm (codeFormula f)))).
imports: Coq(Ensembles) Coq(List) Coq(Arith) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folReplace) hydras.Ackermann(folLogic3) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) Goedel(fixPoint) hydras.Ackermann(NN2PA) Goedel(codeSysPrf) hydras.Ackermann(PAtheory) hydras.Ackermann(code) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) Goedel(rosserPA)