proposition: Lemma freeVarClosed : forall (x : fol.Formula L) (v : nat), ~ In v (freeVarF (close x)).
proof: Proof. intros x v; unfold close; destruct (In_dec eq_nat_dec v (nodup eq_nat_dec (freeVarF x))) as [i | n]. - apply freeVarClosedList1; assumption. - intro H; elim n. rewrite nodup_In. eapply freeVarClosedList2; apply H. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)