proposition: Lemma WF_chain_SCC_trivial : forall i, SCC'_list i = nil -> WF (hd_red_Mod_SCC' i).
proof: Proof. intros. eapply WF_incl. apply chain_SCC'_red_Mod. rewrite H. apply red_Mod_SCC_trivial_empty. 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)