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