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