proposition: Lemma GS : SysPrf T (iffH G (notH (box G))).
proof: Proof. unfold G. destruct (FixPointLNT (notH (LNN2LNT_formula codeSysPf)) 0) as [x [H H0]]. unfold box; apply sysExtend with PA. - assumption. - rewrite <- (subFormulaNot LNT); apply H. Qed.
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)