proposition: Lemma hd_red_mod_empty_incl_hd_red : hd_red_mod nil R << hd_red R.
proof: Proof. unfold inclusion. intros. do 2 destruct H. ded (red_empty H). subst x0. exact H0. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)