proposition: Lemma path_restriction : forall R (y : A) l x, path R x y l -> path (restriction R (x::y::l)) x y l.
proof: Proof. unfold restriction. induction l; simpl; intros. tauto. split. tauto. simpl in IHl. apply path_preserved with (fun x0 y0 : A => (a = x0 \/ y = x0 \/ In x0 l) /\ (a = y0 \/ y = y0 \/ In y0 l) /\ R x0 y0). repeat intro. tauto. apply IHl. tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)