Lemma gevalhom_is_unique {a: algebra σ} (f: term_algebra σ ↷ a): pr1 f = pr1 (gevalhom a). Proof. induction f as [f fishom]. apply funextsec. intro s. apply funextfun. intro t. apply (term_ind (λ s t, f s t = geval a s t)). unfold term_ind_HP. intros. change (build_gterm nm v) with (ops (term_algebra σ) nm v) at 1. rewrite fishom. rewrite gevalstep. apply maponpaths. unfold starfun. apply h1map_path. exact IH. Qed.
Require Import UniMath.Foundations.All.