proposition: Lemma starcomp {S: UU} {X Y Z: sUU S} (f: Y s→ Z) (g: X s→ Y) (l: list S) (x: X⋆ l) : (f s∘ g)⋆⋆ _ x = f⋆⋆ _ (g⋆⋆ _ x).
proof: Proof. unfold starfun. apply pathsinv0. apply h1map_compose. Defined.
imports: UniMath.Foundations.All UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.HVectors