proposition: Lemma staridfun {S: UU} {X: sUU S} (l: list S) (x: X⋆ l): (idsfun X)⋆⋆ _ x = idsfun X⋆ _ x.
proof: Proof. apply h1map_idfun. Defined.
imports: UniMath.Foundations.All UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.HVectors