Definition make_vec {n} (f : ⟦ n ⟧ → A) : vec A n. Proof. induction n as [|m h]. - exact [()]. - exact ((f firstelement) ::: (h (drop f))). Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.