proposition: Lemma path_app_elim_right : forall y z l l' x, path x z (l++y::l') -> path y z l'.
proof: Proof. induction l; simpl; intros. tauto. apply IHl with a. tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)