fact: Parameter subterm_in_subterm : forall p q s t u, subterm_at_pos t p = Some s -> subterm_at_pos s q = Some u -> subterm_at_pos t (p ++ q) = Some u.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)