fact: Fixpoint freeVarListFormula (l : fol.Formulas L) : list nat := match l with | nil => nil (A:=nat) | f :: l => freeVarF f ++ freeVarListFormula l end.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)