proposition: Lemma SCC_in_cycle : forall x y, SCC x y -> exists l, cycle R x l /\ In y l.
proof: Proof. intros. destruct H. apply clos_trans_path in H; apply clos_trans_path in H0. destruct H; destruct H0. exists (x0++y::x1). split; auto with *. unfold cycle. apply path_app; auto. Qed.
imports: CoLoR(Cycle Path ListUtil RelUtil LogicUtil)