proposition: Lemma FirstIncompletenessA : SysPrf T G -> Inconsistent LNN T.
proof: Proof. unfold G; intro H. destruct (FixPointLNN (notH codeSysPf) 0) as [x [H1 H2]]. unfold Inconsistent in |- *. intros f; apply contradiction with x. - assumption. - apply impE with (notH (substF (notH codeSysPf) 0 (codeNatToTerm.natToTermLNN (codeFNN x)))). + apply cp2, iffE1; apply sysExtend with NN; auto. + rewrite (subFormulaNot LNN); apply nnI; now apply codeSysPfCorrect. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) Goedel(fixPoint codeSysPrf) hydras.Ackermann(wConsistent) hydras.Ackermann(NN) hydras.Ackermann(code) hydras.Ackermann(checkPrf) hydras(Compat815)