fact: Definition h1const_vec_h1const {A: UU} {n: nat} {B: A} {P: A → UU} (hv: hvec (vec_map P (vec_fill B n)) ) : vec_to_h1const (h1const_to_vec hv) = hv.
imports: UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Induction.PolynomialFunctors UniMath.Induction.W.Core UniMath.Induction.W.Wtypes UniMath.Induction.FunctorAlgebras_legacy UniMath.Algebra.Universal.Signatures UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.HVectors UniMath.Algebra.Universal.Terms