Definition beta: ind P e_s (sup x f) = e_s x f (λ u, ind P e_s (f u)). Proof. revert P x f e_s. use (invweq (weqonsecbase (λ pred, ∏ x f e_s, ind pred e_s (sup x f) = e_s x f (λ u : B x, ind pred e_s (f u))) lower_predicate)). intro P. cbn beta. intro nm. use (invweq (weqonsecbase (λ hponSub , ∏ e_s, ind (lower_predicate P) e_s (sup nm hponSub) = e_s nm hponSub (λ u : B nm, ind (lower_predicate P) e_s (hponSub u))) (gtweq_sec nm))). intro v. cbn beta. use (invweq (weqonsecbase (λ hpi, ind (lower_predicate P) hpi (sup nm (gtweq_sec nm v)) = hpi nm (gtweq_sec nm v) (λ u : B nm, ind (lower_predicate P) hpi (gtweq_sec nm v u))) (HP_weq P))). intro R. cbn beta. use beta_simplecase. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Induction.PolynomialFunctors. Require Import UniMath.Induction.W.Core. Require Import UniMath.Induction.W.Wtypes. Require Import UniMath.Induction.FunctorAlgebras_legacy. Require Import UniMath.Algebra.Universal.Signatures. Require Import UniMath.Algebra.Universal.Algebras. Require Import UniMath.Algebra.Universal.HVectors. Require Import UniMath.Algebra.Universal.Terms.