fact: Parameter symb_in_subterm : forall f s t p, subterm_at_pos t p = Some s -> symb_in_term f s = true -> symb_in_term f t = true.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)