Lemma fromtermstep {A: sUU (sorts σ)} {V: varspec σ} (op : (∏ nm : names σ, A⋆ (arity nm) → A (sort nm))) (α : assignment A V) (nm: names σ) (v: (term σ V)⋆ (arity nm)) : fromterm op α (sort nm) (build_term nm v) = op nm ((fromterm op α)⋆⋆ (arity nm) v). Proof. unfold fromterm, fromgterm, build_term. rewrite (term_ind_step _ _ (namelift V nm)). simpl. rewrite h2lower_h1map_h1lift. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Algebra.Universal.SortedTypes.