proposition: Lemma 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.
proof: Proof. intro p; induction p as [ | i p]; intros q s t u Sub1 Sub2. simpl in Sub1; injection Sub1; clear Sub1; intros; subst; trivial. simpl in Sub1; simpl; destruct t as [v | f l]. discriminate. destruct (nth_error l i) as [ti | ]. apply IHp with s; trivial. discriminate. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)