proposition: Lemma path_clos_trans : forall y l x, path x y l -> R! x y.
proof: Proof. induction l; simpl; intros. constructor. hyp. constructor 2 with a. constructor. tauto. apply IHl. tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)