proposition: Lemma hel_htl {n} {v: vec UU (S n)} (hv : hvec v) (i : ⟦ n ⟧) : hel (htl hv) i = hdrop (hel hv) i.
proof: Proof. apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors