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