proposition: Lemma hd_red_Mod_remdup : hd_red_Mod S R << hd_red_Mod S (remdup (@eq_rule_dec Sig) R).
proof: Proof. intros. unfold hd_red_Mod. comp. unfold inclusion. intros. redtac. ex l r s. split_all. apply incl_remdup. auto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)