proposition: Lemma rtc_red_maxvar : forall t u, red R # t u -> maxvar u <= maxvar t.
proof: Proof. induction 1. apply red_maxvar. hyp. lia. lia. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)