fact: Fixpoint var_list (t : term) : list variable := match t with | Var x => (x :: nil) | Term _ l => let var_list_list := (fix 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) in var_list_list l end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)