Lemma el_vec_fill {A: UU} (a: A) {n:nat} (i:⟦ n ⟧) : el (vec_fill a n) i = a. Proof. induction n as [ | n IHn]. + use (fromstn0 i). + induction i as [i ilt]. induction i as [| i IHi]. - apply idpath. - use IHn. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.