proposition: Lemma SCC'_list_exact : forall i r, In r (SCC'_list i) <-> SCC'_tag HM r = Some i.
proof: Proof. intros; split; intro. unfold SCC'_list in H. rewrite SCC'_list_aux_exact in H. tauto. unfold SCC'_list; rewrite SCC'_list_aux_exact; split; try tauto. assert (SCC' r r). rewrite (SCC'_tag_exact hyps HM). intuition. congruence. unfold SCCTopoOrdering.SCC' in H0. 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)