fact: Fixpoint symb_in_term_list f (l : list term) {struct l} : bool := match l with | nil => false | t :: lt => orb (symb_in_term f t) (symb_in_term_list f lt) end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)