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