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