proposition: Lemma WF_hd_red_Mod_empty : WF (hd_red_Mod S nil).
proof: Proof. apply WF_incl with empty_rel. intros x y h. redtac. contr. apply WF_empty_rel. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)