proposition: Lemma WF_red_mod_empty : WF (red_mod E nil).
proof: Proof. intro x. apply SN_intro. intros y Exy. destruct Exy as [z [xz zy]]. redtac. contr. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)