proposition: Lemma red_mod_fill : forall t u c, 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 context_closed_rtc. unfold context_closed. apply red_fill. hyp. apply red_fill. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)