proposition: Lemma red_rule : forall l r c, In (mkRule l r) R -> red R (fill c l) (fill c r).
proof: Proof. intros. unfold red. exists l. exists r. exists c. auto. Qed.
imports: CoLoR(LogicUtil RelUtil ListUtil BoolUtil EqUtil ListDec)