proposition: Lemma Vmap_term_int_fval : forall v n k (ts : terms k), n > maxvars ts -> Vmap (term_int (fval v n)) ts = Vmap (term_int v) ts.
proof: Proof. induction ts. refl. simpl. rewrite maxvars_cons, gt_max. intuition. rewrite H, <- term_int_eq_fval_lt. refl. hyp. Qed.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)