proposition: Lemma clos_trans_path : forall x y, R! x y -> exists l, path x y l.
proof: Proof. intros. induction H. exists (nil : list A). simpl. hyp. destruct IHclos_trans1. destruct IHclos_trans2. exists (x0++y::x1). apply path_app; hyp. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)