proposition: Lemma hd_red_incl_hd_red_mod : hd_red R << hd_red_mod nil R.
proof: Proof. intros u v Ruv. exists u. split. constructor 2. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)