Definition beta_simplecase : ind lowP e_s (sup nm f) = (e_s nm f (λ u, ind lowP e_s (f u))). Proof. use (weqonpaths2 _ _ _ (term_ind_step P R nm v)). + apply ind_HP_Th. + etrans. { apply ind_HP_Th_termInd. } use toforallpaths. use (!termInd_ind). + rewrite UnderstandingR. unfold funcomp. use pathsweq1'. use maponpaths. use maponpaths. use ind_HP_Hypo_h2map. 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.