proposition: Lemma restricted_path_incl : is_restricted R l -> forall m x y, path R x y m -> x :: m ++ y :: nil [= l.
proof: Proof. induction m; simpl; intros. ded (H _ _ H0). unfold is_restricted in H. unfold List.incl. simpl. intuition. subst a. exact H2. subst a. exact H3. destruct H0. apply incl_cons. ded (H _ _ H0). unfold is_restricted in H2. intuition. apply IHm. exact H1. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)