proposition: Lemma red_incl_red_mod : red R << red_mod nil R.
proof: Proof. intros u v Ruv. exists u. split. constructor 2. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)