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