proposition: Lemma freeVarCodeSysPrfN : forall v : nat, In v (freeVarF codeSysPrfNot) -> v <= 1.
proof: Proof. intros v H; unfold codeSysPrfNot in H. SimplFreeVar. - apply freeVarCodeSysPrf. apply H. - assert (H0: Representable NN 1 codeNot (primRecFormula 1 (proj1_sig codeNotIsPR))) by apply primRecRepresentable. destruct H0 as [H0 _]; now apply H0. - rewrite <- H; apply Nat.le_0_l. 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)