proposition: Lemma freeVarG : closed G.
proof: Proof. unfold closed, G. destruct (FixPointLNN (notH codeSysPf) 0) as [x [H1 H2]]. unfold not in |- *; intros. destruct (H2 v) as [H0 H3]; rename H3 into foo; rename H0 into H3. absurd (v = 0). - eapply in_remove_neq; apply H3; assumption. - eapply (freeVarCodeSysPf LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsPR codeArityLNNRIsPR). + apply freeVarRepT. + assert (H5:(forall f : Formula, In v (freeVarF (notH f)) -> In v (freeVarF f))). { intros f H5; apply H5. } apply H5; eapply in_remove. unfold codeSysPf in H3; apply H3; assumption. 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)