Lemma vec_extens {n} {u v : vec A n} : (∏ i : ⟦ n ⟧, el u i = el v i) → u = v. Proof. intros H. induction n as [|m meq]. - apply vec0_eq. - apply vecS_eq. + exact (H firstelement). + apply meq. intros. do 2 rewrite el_tl. apply H. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.