proposition: Lemma nodup_SCC'_list_aux : forall i L, nodup L -> nodup (SCC'_list_aux i L).
proof: Proof. induction L; intros; simpl. tauto. simpl in H. destruct H. destruct (eq_opt_dec eq_nat_dec (SCC'_tag HM a) (Some i)); try tauto. split. rewrite SCC'_list_aux_exact. tauto. tauto. 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)