proposition: Lemma WF_SCC'_union : (forall i, i < dim -> WF (hd_red_Mod_SCC' i)) -> WF (hd_red_Mod S R).
proof: Proof. intros. eapply WF_incl. apply hd_red_Mod_SCC'_cover. unfold hd_red_Mod_SCC'_union, sorted_hd_red_Mod_SCC'. eapply WF_SCC'_union_aux. intros. apply H. apply s_SCC's_spec_bound. auto. unfold s_SCC's; destruct sorted_SCC'. simpl in *. 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)