Lemma hel_make_hvec_fun {n} {v: vec UU n} (f : ∏ i: ⟦ n ⟧, el v i) : hel (make_hvec f) = f. Proof. apply funextsec. apply hel_make_hvec. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.