proposition: Lemma SCC'_sym : forall x y ,SCC' x y -> SCC' y x.
proof: Proof. intros; destruct H. split; try tauto. destruct H. left; auto. right; apply SCC_sym; auto. Qed.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)