proposition: Lemma red_sub : forall t u s, red R t u -> red R (sub s t) (sub s u).
proof: Proof. intros. redtac. subst. rewrite !sub_fill, !sub_sub. apply red_rule. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)