proposition: Lemma rtc_red_fill : forall c t u, red R # t u -> red R # (fill c t) (fill c u).
proof: Proof. induction 1. apply rt_step. apply red_fill. hyp. apply rt_refl. apply rt_trans with (fill c y); hyp. Qed.
imports: CoLoR(LogicUtil RelUtil ListUtil BoolUtil EqUtil ListDec)