proposition: Theorem ind_HP_Hypo : hvec (h1map_vec P v) ≃ (∏ u : B nm, lowP (f u)).
proof: Proof. use (weqcomp helf_weq). use weqonsecfibers. intro i. use eqweqmap. use hel_h1map_vec_vec_fill. Defined.
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