fact: Fixpoint symb_list (t : term) : list symbol := match t with | Var x => nil | Term f l => let symb_list_list := (fix symb_list_list (l : list term) {struct l} : list symbol := match l with | nil => nil | t :: lt => symb_list t ++ symb_list_list lt end) in f :: (symb_list_list l) end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)