proposition: Lemma hd_red_incl_red : hd_red R << red R.
proof: Proof. unfold inclusion. intros. redtac. subst x. subst y. apply red_rule_top. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)