proposition: Lemma gevalstep {a: algebra σ} (nm: names σ) (v: (gterm σ)⋆ (arity nm)) : geval a _ (build_gterm nm v) = ops a nm (h1map (geval a) v).
proof: Proof. unfold geval. apply fromtermstep. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Terms