proposition: Lemma sub_path : forall l x y x' y' l' m p, x::l++y::nil = m++x'::l'++y'::p -> path x y l -> path x' y' l'.
proof: Proof. induction l; simpl; intros. destruct m; simpl in H. injection H; intros. subst x'. destruct l'; simpl in H1. injection H1; intros. subst y'. exact H0. injection H1; intros. destruct l'; discr. injection H; intros. destruct m; simpl in H1. injection H1; intros. destruct l'; discr. injection H1; intros. destruct m; discr. destruct H0. destruct m; simpl in H. injection H; intros. subst x'. destruct l'; simpl in H2; simpl in H. injection H2; intros. subst a. exact H0. simpl. injection H2; intros. subst a0. intuition. apply (IHl a y a y' l' nil p). simpl. exact H2. exact H1. injection H; intros. subst a0. eapply IHl. apply H2. exact H1. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)