proposition: Lemma red_Rules (R : list rule) : red (of_list R) == ATrs.red R.
proof: Proof. split; intros t u H. redtac. subst. apply ATrs.red_rule. hyp. ATrs.redtac. subst. apply red_rule. hyp. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)