Lemma hel_hcons_hhd {n} {v: vec UU n} (hv : hvec v) {X:UU} (x : X) : hel (x ::: hv) (firstelement) = x. Proof. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.