Definition universalmap: ∑ h: free_algebra σ V ↷ a, ∏ v: V, h _ (varterm v) = α v. Proof. exists evalhom. intro v. simpl. unfold eval, varterm. apply fromtermstep'. Defined.
Require Import UniMath.Foundations.All.