proposition: Lemma path_app_elim : forall l x y z m, path x y (l++z::m) -> path x z l /\ path z y m.
proof: Proof. induction l; simpl; intros. exact H. destruct H. ded (IHl _ _ _ _ H0). intuition. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)