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