Definition hel_h1map_vec_vec_fill : el (h1map_vec f hv) i = f a (eqweqmap (el_vec_map_vec_fill P a i) (hel hv i)). Proof. etrans. { apply hel_h1map_vec. } use hel_h1map_vec_vec_fill_lemma. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.