proposition: Lemma vec_extens {n} {u v : vec A n} : (∏ i : ⟦ n ⟧, el u i = el v i) → u = v.
proof: 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.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers