fact: Fixpoint var_list_list (l : list term) {struct l} : list variable := match l with | nil => nil | t :: lt => var_list t ++ var_list_list lt end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)