Definition functionToList n : (stn n -> A) -> list. Proof. intros f. exact (n ,, make_vec f). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.