proposition: Lemma 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.
proof: Proof. intro p; induction p as [ | i p]; intros q s t Sub. exists t; split; trivial. simpl in Sub; destruct t as [v | f l]. discriminate. generalize (nth_error_ok_in i l); destruct (nth_error l i) as [ti | ]. intro H; destruct (H _ (eq_refl _)) as [l1 [l2 [L H']]]; clear H. destruct (IHp q s ti Sub) as [u [Sub' H'']]. exists u; subst; simpl; rewrite nth_error_at_pos; split; 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)