proposition: Lemma path_shrink : forall y l' x, path x y l' -> path x y (shrink eqdec l').
proof: Proof. induction l'; simpl; intros. hyp. assert (path a y (shrink eqdec l')). apply IHl'; tauto. destruct (In_dec eqdec a (shrink eqdec l')). apply path_cut_bis; tauto. simpl. tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)