Lemma hel_make_hvec {n} {v: vec UU n} (f : ∏ i: ⟦ n ⟧, el v i) : hel (make_hvec f) ~ f . Proof. intro i. induction n as [|m meq]. - exact (fromstn0 i). - induction i as (j,jlt). induction j as [|k _]. + use (stn_predicate (λ z , hel (make_hvec f) z = f z) 0 _ jlt). { reflexivity. } apply idpath. + use meq. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.