fact: Parameter var_list_unfold : forall t, var_list t = match t with | Var x => (x :: nil) | Term _ l => var_list_list l end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)