proposition: Lemma hd_red_rule (R : rules) l r s : R (mkRule l r) -> hd_red R (sub s l) (sub s r).
proof: Proof. intro. unfold hd_red. ex l r s. auto. Qed.
imports: CoLoR(ATrs ListUtil RelUtil ARelation LogicUtil SetUtil) Coq(Morphisms)