proposition: Lemma red_Mod_SCC_trivial_empty : WF (hd_red_Mod S nil).
proof: Proof. unfold WF; intro; apply SN_intro; intros. do 2 destruct H. do 4 destruct H0. simpl in *; 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)