proposition: Lemma red_rule_top : forall l r, In (mkRule l r) R -> red R l r.
proof: Proof. intros. red. exists l. exists r. exists (mkContext nil nil). repeat split; unfold fill; simpl; trivial || rewrite <- app_nil_end; trivial. Qed.
imports: CoLoR(LogicUtil RelUtil ListUtil BoolUtil EqUtil ListDec)