fact: Parameter symb_in_direct_subterm : forall f l t g, In t l -> symb_in_term g t = true -> symb_in_term g (Term f l) = true.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)