proposition: Lemma hd_red_mod_Rules (E R : list rule) : hd_red_mod (of_list E) (of_list R) == ATrs.hd_red_mod E R.
proof: Proof. intros. unfold hd_red_mod, ATrs.hd_red_mod. rewrite !red_Rules, !hd_red_Rules. refl. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)