proposition: Lemma maxvar_lmax : forall t, maxvar t = lmax (vars t).
proof: Proof. intro t. pattern t. set (Q := fun n (ts : terms n) => maxvars ts = lmax (vars_vec ts)). apply term_ind with (Q := Q); clear t. intros x; simpl; now rewrite Nat.max_0_r. intros f ts H. rewrite maxvar_fun, vars_fun. hyp. unfold Q. auto. intros t n ts H1 H2. unfold Q. simpl. rewrite lmax_app. unfold Q in H2. rewrite maxvars_cons, H1, H2. refl. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)