Lemma evalstep (nm: names σ) (v: (term σ V)⋆ (arity nm)) : eval (sort nm) (build_term nm v) = ops a nm (eval⋆⋆ (arity nm) v). Proof. unfold eval. change (sort nm) with (sort nm). apply fromtermstep. Defined.
Require Import UniMath.Foundations.All.