proposition: Lemma vmap_insert {A B} (f : A → B) (n : nat) i x (v : vec A n) : vmap f (vinsert i x v) = vinsert i (f x) (vmap f v).
proof: Proof. induction v; inv_fin i; intros; f_equal/=; auto. Qed.
imports: stdpp(countable) stdpp(options)