Definition make_hvec {n: nat} {v: vec UU n} (f: ∏ i: ⟦ n ⟧, el v i) : hvec v. Proof. revert n v f. use vec_ind. + intro. exact tt. + intros X n v IH f. exists (f firstelement). exact (IH (hdrop f)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.