proposition: Theorem toLowerPredicateWeq : (∏ (s : sorts σ) (t : gterm σ s), P s t) ≃ (∏ w : U, lowP w).
proof: Proof. use weqsecoverunit. 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