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