Lemma term_ind_step (P: ∏ (s: sorts σ), term σ s → UU) (R: term_ind_HP P) (nm: names σ) (v: (term σ)⋆ (arity nm)) : term_ind P R (build_term nm v) = R nm v (h2map (λ s t q, term_ind P R t) (h1lift v)). Proof. unfold term_ind. set (princop_sorteq_idpath := princop_sorteq_buildterm nm v). set (t := build_term nm v) in *. simpl (length t). unfold term_ind_onlength at 1. rewrite nat_rect_step. set (v0len := subterms_length t). set (v0norm := term_normalization t). clearbody v0len v0norm. change (princop t) with nm in *. induction (! (subterms_build_term nm v: subterms t = v)). induction (! princop_sorteq_idpath). change (build_term nm v = t) in v0norm. assert (v0normisid: v0norm = idpath _). { apply proofirrelevance. apply isasetterm. } induction (! v0normisid). rewrite idpath_transportf. rewrite paths_rect_step. apply maponpaths. rewrite (h1map_h1lift_as_h2map v v0len). apply (maponpaths (λ x, h2map x _)). repeat (apply funextsec; intro). apply (term_ind_onlength_nirrelevant P R (pr1 (vecoplist2oplist (h1map_vec (λ x2 : sorts σ, term2oplist) v)))). - apply isreflnatleh. - apply natlthsntoleh. apply x1. Defined.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.