Definition subterms {s: sorts σ} (t: term σ s): (term σ)⋆ (arity (princop t)) := pr12 (term_decompose t). Local Definition subterms_length {s: sorts σ} (t: term σ s) : hvec (h1map_vec (λ _ t', hProptoType (length (term2oplist t') < length t)) (subterms t)) := pr122 (term_decompose t). Local Definition princop_sorteq {s: sorts σ} (t: term σ s): sort (princop t) = s := pr122 (pr2 (term_decompose t)). Local Definition oplist_normalization {s: sorts σ} (t: term σ s) : term2oplist (build_term (princop t) (subterms t)) = t := pr222 (pr2 (term_decompose t)). Local Lemma princop_sorteq_buildterm (nm: names σ) (v: (term σ)⋆ (arity nm)) : princop_sorteq (build_term nm v) = idpath (sort nm). Proof. apply proofirrelevance. apply isasetifdeceq. apply decproperty. Defined.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.