proposition: Lemma vec_to_list_map `(f : A → B) {n} (v : vec A n) : vec_to_list (vmap f v) = f <$> vec_to_list v.
proof: Proof. induction v as [|??? IHv]; simpl; [done|]. by rewrite IHv. Qed.
imports: stdpp(countable) stdpp(options)