proposition: Lemma red_mod_empty_incl_red : red_mod nil R << red R.
proof: Proof. unfold inclusion. intros. redtac. ded (red_nil_rtc H). subst. apply red_rule. exact H0. Qed.
imports: CoLoR(LogicUtil RelUtil ListUtil BoolUtil EqUtil ListDec)