proposition: Lemma hd_red_mod_incl_red_mod : forall E, hd_red_mod E R << red_mod E R.
proof: Proof. intro. unfold hd_red_mod, red_mod. comp. apply hd_red_incl_red. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)