fact: Fixpoint symb_in_term (f : symbol) (t:term) : bool := match t with | Var _ => false | Term g l => let symb_in_term_list := (fix 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) in orb (eq_symb_bool f g) (symb_in_term_list f l) end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)