proposition: 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: Proof. unfold fromterm, fromgterm, varterm. rewrite (term_ind_step _ _ (varname v)). apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Terms