proposition: Lemma hd_red_Mod_SCC'_cover : hd_red_Mod S R << hd_red_Mod_SCC'_union.
proof: Proof. unfold inclusion. intros. unfold hd_red_Mod_SCC'_union in H. unfold hd_red_Mod in H. do 2 destruct H. ded (hd_red_SCC'_cover H0). destruct H1 as [i]. assert (hd_red_Mod_SCC' i x y). exists x0; tauto. unfold hd_red_Mod_SCC'_union. eapply union_list_spec; eauto. unfold sorted_hd_red_Mod_SCC'. apply in_map. apply s_SCC's_spec_cover; 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)