proposition: Lemma hd_red_mod_of_hd_red_Mod_int : hd_red_Mod (int_red E #) R << hd_red_mod E R.
proof: Proof. unfold hd_red_Mod, hd_red_mod. apply compose_incl. assert (int_red E # << red E #). apply rtc_incl. apply int_red_incl_red. eauto. refl. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)