Definition functionToList' n : (stn n -> A) -> vec A n. Proof. intros f. induction n as [|n I]. - exact tt. - exists (f (●0))%stn. exact (I(f ∘ dni (●0)))%stn. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.