proposition: Lemma maxvar_in : forall x t n (v : terms n), x <= maxvar t -> Vin t v -> x <= maxvars v.
proof: Proof. induction v; unfold maxvars; simpl; intros. contr. destruct H0. subst t. apply le_max_intro_l. hyp. apply le_max_intro_r. apply IHv; hyp. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)