proposition: Lemma evalstep (nm: names σ) (v: (term σ V)⋆ (arity nm)) : eval (sort nm) (build_term nm v) = ops a nm (eval⋆⋆ (arity nm) v).
proof: Proof. unfold eval. change (sort nm) with (sort nm). apply fromtermstep. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.VTerms