Lemma inv_helf_weq {n:nat} {v:vec UU n} : invmap (helf_weq (n:=n) (v:=v)) = make_hvec. Proof. use funextsec. intro. use (invmaponpathsweq helf_weq). rewrite homotweqinvweq. simpl. rewrite hel_make_hvec_fun. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.