proposition: Lemma red_mod_empty_incl_red : red_mod nil R << red R.
proof: Proof. intros u v Ruv. destruct Ruv as [s' [ss' Ruv]]. rewrite (red_empty ss'). hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)