proposition: Lemma path_restricted_incl : forall y l l' x, is_restricted R l -> path x y l' -> l' [= l.
proof: Proof. unfold is_restricted. induction l'; simpl; intros. intro. simpl. tauto. apply incl_cons. pose (H x a). tauto. apply IHl' with a; tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)