proposition: Lemma WF_hd_red_mod_empty : WF (hd_red_mod E nil).
proof: Proof. apply WF_incl with (red_mod E nil). apply hd_red_mod_incl_red_mod. apply WF_red_mod_empty. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)