proposition: Lemma cycle_in_SCC : forall x l, cycle R x l -> forall y, In y l -> SCC x y.
proof: Proof. intros. unfold SCC. unfold cycle in H. gen (in_elim H0); intros. destruct H1; destruct H1; subst. apply path_app_elim in H. destruct H. apply path_clos_trans in H; apply path_clos_trans in H1. split; auto. Qed.
imports: CoLoR(Cycle Path ListUtil RelUtil LogicUtil)