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