proposition: Lemma WF_SCC'_union_aux : forall L, (forall i, In i L -> WF (hd_red_Mod_SCC' i)) -> sort RT_ODPG L -> WF (fold_right (@union _) empty (map hd_red_Mod_SCC' L)).
proof: Proof. intros. induction L; simpl in *. intro. apply SN_intro. intros; tauto. inversion H0. subst a0; subst l. eapply WF_incl. apply union_commut. apply WF_union_commut. apply IHL. intros. apply H. right; auto. destruct H0; auto. apply H. left; auto. unfold inclusion. intros. cut False; try tauto. destruct H1 as [z]. destruct H1. ded (union_list_spec2 _ _ _ H1). destruct H5 as [r]. destruct H5. assert (exists b, In b L /\ r = hd_red_Mod_SCC' b). apply in_map_elim; auto. destruct H7 as [b]. destruct H7; subst r. cut (RT_ODPG a b). intro. eapply (compose_empty H8). exists z; eauto. eapply sort_transitive. unfold RT; destruct topo_sortable_Rquo'. simpl in *. ded (l (nats_decr_lt dim)). destruct H8. intuition. ehyp. 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)