Lemma fromtermstep {A: sUU (sorts σ)} (nm: names σ) (op : ∏ (nm : names σ), A⋆ (arity nm) → A (sort nm)) (v: (term σ)⋆ (arity nm)) : fromterm op (build_term nm v) = op nm (h1map (@fromterm A op) v). Proof. unfold fromterm. rewrite term_ind_step. rewrite h2lower_h1map_h1lift. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.