proposition: Lemma red_mod0_maxvar : forall t u, red_mod0 E R t u -> maxvar u = 0.
proof: Proof. intros. destruct H. cut (maxvar u <= maxvar t). lia. apply (red_mod_maxvar hE hR H). Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)