proposition: 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: Proof. unfold fromterm. rewrite term_ind_step. rewrite h2lower_h1map_h1lift. apply idpath. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Combinatorics.Maybe UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures