Definition term_ind_HP (P: ∏ (s: sorts σ), term σ s → UU) := ∏ (nm: names σ) (v: (term σ)⋆ (arity nm)) (IH: hvec (h1map_vec P v)) , P (sort nm) (build_term nm v). Local Lemma term_ind_onlength (P: ∏ (s: sorts σ), term σ s → UU) (R: term_ind_HP P) : ∏ (n: nat) (s: sorts σ) (t: term σ s), length t ≤ n → P s t. Proof. induction n. - intros s t tlen. exact (term_notnil tlen). - intros s t tlen. apply (transportf _ (term_normalization t)). induction (princop_sorteq t). change (P (sort (princop t)) (build_term (princop t) (subterms t))). apply (R (princop t) (subterms t)). refine (h2map _ (subterms_length t)). intros. apply IHn. apply natlthsntoleh. eapply natlthlehtrans. + exact X. + exact tlen. Defined.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.