proposition: Lemma path_preserved : forall R R' (y : A) l x, R << R' -> path R x y l -> path R' x y l.
proof: Proof. induction l; repeat intro; simpl in H0 |- * . apply H. hyp. split. pose (H x a). tauto. pose (IHl a). tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)