proposition: Lemma path_cut_bis : forall l' x y z, In z l' -> R x z -> path z y l' -> path x y (cut eqdec z l').
proof: Proof. intros. rewrite (cut_head eqdec z l'). simpl. assert (path z y (tail (cut eqdec z l'))). apply path_cut; hyp. destruct l'. pose (in_nil H). contr. tauto. hyp. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)