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; try split; try tauto. destruct H; destruct H0; subst; auto. left; auto. right; auto. right; auto. right; eapply SCC_trans. eauto. hyp. Qed.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)