Lemma gevalstep {a: algebra σ} (nm: names σ) (v: (gterm σ)⋆ (arity nm)) : geval a _ (build_gterm nm v) = ops a nm (h1map (geval a) v). Proof. unfold geval. apply fromtermstep. Defined.
Require Import UniMath.Foundations.All.