proposition: Lemma red0_maxvar : forall t u, red0 R t u -> maxvar u = 0.
proof: Proof. unfold red0. split_all. cut (maxvar u <= maxvar t). lia. apply (red_maxvar hR H). Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)