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