proposition: Lemma path_cycle : forall x y l, path R x y l -> In x l -> exists m, exists p, l = m ++ x :: p /\ cycle x m.
proof: Proof. intros. ded (in_elim H0). do 2 destruct H1. subst l. ded (path_app_elim H). destruct H1. exists x0. exists x1. intuition. Qed.
imports: Coq(Relations) CoLoR(LogicUtil Path ListUtil ListNodup)