proposition: Theorem HP_weq : term_ind_HP P ≃ ind_HP (lowP).
proof: Proof. use weqonsecfibers. intro x. cbn beta. use weqonsec. + use gtweq_sec. + intro v. use weqonsec. - use ind_HP_Hypo. - intro HypOnSub. use ind_HP_Th. 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