proposition: Lemma red_mod_fill : forall c t u, red_mod E R t u -> red_mod E R (fill c t) (fill c u).
proof: Proof. intros. do 2 destruct H. exists (fill c x); split. apply rtc_red_fill. hyp. apply red_fill. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil ListUtil BoolUtil EqUtil ListDec)