proposition: Lemma chain_SCC'_red_Mod : forall i, hd_red_Mod_SCC' i << hd_red_Mod S (SCC'_list i).
proof: Proof. unfold inclusion; intros. do 2 destruct H. exists x0. split. auto. unfold hd_red_SCC' in H0. unfold hd_red. do 3 destruct H0. exists x1; exists x2; exists x3. rewrite SCC'_list_exact. intuition. 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)