proposition: Lemma vars_max : forall x t, In x (vars t) -> x <= maxvar t.
proof: Proof. intros x t. pattern t. apply term_ind with (Q := fun n (ts : terms n) => In x (vars_vec ts) -> x <= maxvars ts); clear t; intros. simpl in *. intuition. rewrite maxvar_fun. rewrite vars_fun in H0. auto. contr. simpl in *. destruct (in_app_or H1); unfold maxvars; simpl. apply le_max_intro_l. auto. apply le_max_intro_r. auto. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)