Theorem ind_HP_Hypo_h2map : ind_HP_Hypo P nm v (h2map (λ (s : sorts σ) (t _ : gterm σ s), term_ind P R t) (h1lift v)) = (λ u : B nm, ind lowP e_s (f u)). Proof. use pathsweq1'. unfold ind_HP_Hypo. rewrite invmap_weqcomp_expand. rewrite inv_helf_weq. rewrite inv_weqonsecfibers. unfold funcomp. rewrite termInd_ind. use h2map_makehvec_basevecfill. 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.