proposition: Lemma path_restriction_In_left : forall (x y : A) l', path (restriction R l) x y l' -> In x l.
proof: Proof. unfold restriction. intros; destruct l'; simpl in H; tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)