Lemma hvec_extens {n} {v: vec UU n} {hu hv: hvec v} : (∏ i : ⟦ n ⟧, hel hu i = hel hv i) → hu = hv. Proof. intros H. revert n v hu hv H. use vec_ind. - cbn beta. intros. use proofirrelevance. use isapropunit. - cbn beta. intros X n v IH hv hu H. induction hv as (xv,htv). induction hu as (xu,htu). use dirprod_paths. * use (H firstelement). * use IH. intro i. use (H (dni_firstelement i)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.