proposition: Lemma SCC_trans : forall x y z, SCC x y -> SCC y z -> SCC x z.
proof: Proof. intros. unfold SCC in *. destruct H; destruct H0. split; eapply t_trans; eauto; auto. Qed.
imports: CoLoR(Cycle Path ListUtil RelUtil LogicUtil)