proposition: Lemma nodup_SCC'_list : forall i, nodup (SCC'_list i).
proof: Proof. unfold SCC'_list; intros. apply nodup_SCC'_list_aux. auto. Qed.
imports: Coq(Permutation Multiset Setoid PermutSetoid) CoLoR(SCCTopoOrdering AGraph ATrs RelUtil RelSub BoundNat AdjMat LogicUtil NatUtil SCC SCC_dec ListExtras SN VecUtil GDomainBij OptUtil Union SortUtil ListNodup ListPermutation)