proposition: Lemma red_mod_empty (R : rules) : red_mod empty R == red R.
proof: Proof. unfold red_mod. rewrite rt_red_empty. split; intros t u h. destruct h. intuition. subst. hyp. exists t. auto. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)