Definition hel_h1map_vec_vec_fill_lemma : f (el (vec_fill a n) i) (eqweqmap (el_vec_map P (vec_fill a n) i) (hel hv i)) = f a (eqweqmap (el_vec_map_vec_fill P a i) (hel hv i)). Proof. induction n as [|m IHn0]. + use fromstn0. exact i. + induction hv as [hvhead hvtail]. induction i as [j jlt]. induction j as [| k]. - apply idpath. - use IHn0. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.