proposition: Lemma rt_red_empty : red (@empty rule) # == eq.
proof: Proof. split; intros t u h. elim h; intros. redtac. contr. refl. trans y; hyp. subst. apply rt_refl. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)