proposition: Lemma ishomgeval (a: algebra σ): ishom (geval a).
proof: Proof. red. intros. unfold starfun. apply gevalstep. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Terms