Definition helf_weq {n: nat} {v: vec UU n} : (hvec v) ≃ ∏ i: ⟦ n ⟧, el v i. Proof. use weq_iso. + use hel. + use make_hvec. + use make_hvec_hel. + use hel_make_hvec_fun. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.