proposition: Lemma freeVarCodeSysPf : forall v : nat, In v (freeVarF codeSysPf) -> v = 0.
proof: Proof. intros v H; unfold codeSysPf in H. destruct v as [| n]. - reflexivity. - destruct n. elim (in_remove_neq _ _ _ _ _ H). + reflexivity. + elim (Compat815.le_not_lt (S (S n)) 1). * apply freeVarCodeSysPrf. eapply in_remove, H. * apply Compat815.lt_n_S, Nat.lt_0_succ. 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)