Lemma make_hvec_hel {n} {v: vec UU n} (hv : hvec v) : (make_hvec (hel hv)) = hv . Proof. apply hvec_extens. intros i. rewrite hel_make_hvec. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.