proposition: Lemma notInFreeVarSys : forall x, ~ In_freeVarSys x (Ensembles.Empty_set (fol.Formula L)).
proof: Proof. intros x; unfold In_freeVarSys in |- *. intros [? [? H0]]; destruct H0. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)