proposition: Lemma path_cut : forall y l' x, In x l' -> path x y l' -> path x y (tail(cut eqdec x l')).
proof: Proof. intros. apply path_suffix with l' x. hyp. rewrite <- (cut_head eqdec x l' H). apply suffix_cut. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)