proposition: Lemma red_fill : forall c t u, red R t u -> red R (fill c t) (fill c u).
proof: Proof. intros. redtac. unfold red. exists l. exists r. exists (comp c c0). split. hyp. rewrite !fill_fill. auto. Qed.
imports: CoLoR(LogicUtil RelUtil ListUtil BoolUtil EqUtil ListDec)