[STATEMENT]
lemma map_vec_append: "map_vec f (a @\<^sub>v b) = map_vec f a @\<^sub>v map_vec f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vec f (a @\<^sub>v b) = map_vec f a @\<^sub>v map_vec f b
[PROOF STEP]
by (induction a arbitrary: b) (auto)