proposition: Lemma red_maxvar : forall t u, red R t u -> maxvar u <= maxvar t.
proof: Proof. intros. rewrite !maxvar_lmax. apply incl_lmax. apply red_preserve_vars. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)