proposition: Lemma red_mod_empty : red_mod nil R == red R.
proof: Proof. split. apply red_mod_empty_incl_red. intros t u h. exists t. split. apply rtc_refl. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)