proposition: Lemma Vmap_map_sum : forall m s, (forall x, x <= m -> s x = Var x) -> forall n (ts : terms n), maxvars ts <= m -> forall v, Vmap (sub s) (Vmap_sum (Vmap capa ts) v) = Vmap_sum (Vmap capa ts) (Vmap (sub s) v).
proof: Proof. induction ts; simpl; intros. refl. gen (Vbreak_eq_app v). intro. rewrite H1, Vmap_app, !Vbreak_app. simpl. rewrite maxvars_cons in H0. apply Vcons_eq_intro. eapply app_fcap. apply H. eapply le_max_elim_l. apply H0. apply IHts. eapply le_max_elim_r. apply H0. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)