proposition: Lemma maxvar_le_fun : forall m f ts, maxvar (Fun f ts) <= m -> Vforall (maxvar_le m) ts.
proof: Proof. intros until ts. rewrite maxvar_fun. intro. gen (Vmax_forall H). clear H. intro H. gen (Vforall_map_elim H). intuition. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)