proposition: Lemma vec_to_list_take {A n} i (v : vec A n) : vec_to_list (vtake i v) = take (fin_to_nat i) (vec_to_list v).
proof: Proof. induction i; inv_vec v; intros; f_equal/=; auto. Qed.
imports: stdpp(countable) stdpp(options)