proposition: Lemma red_fill : forall t u c, red R t u -> red R (fill c t) (fill c u).
proof: Proof. intros. redtac. unfold red. ex l r (AContext.comp c c0) s. split. hyp. subst t. subst u. rewrite !fill_fill. auto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)