proposition: Lemma red_mod_maxvar : forall t u, red_mod E R t u -> maxvar u <= maxvar t.
proof: Proof. intros. do 2 destruct H. trans (maxvar x). apply (red_maxvar hR H0). apply (rtc_red_maxvar hE H). Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)