English
Fix.rec is the unique morphism into β given a recursive definition: if g and h agree on Fix.mk x for all x, then Fix.rec g = h.
Русский
Fix.rec единственна по отношению к отображению; если два отображения совпадают на конструкторе Fix.mk, то они совпадают на всех элементах.
LaTeX
$$$\forall {g : F (\alpha.append1 \beta) \to \beta} (h : \mathrm{Fix} F \alpha \to \beta),\; (\forall x, h(\mathrm{Fix.mk} x) = g(\mathrm{appendFun} id h <$$> x)) \Rightarrow \mathrm{Fix.rec} \ g = h$$$
Lean4
theorem rec_unique {β : Type u} (g : F (append1 α β) → β) (h : Fix F α → β)
(hyp : ∀ x, h (Fix.mk x) = g (appendFun id h <$$> x)) : Fix.rec g = h :=
by
ext x
apply Fix.ind_rec
intro x hyp'
rw [hyp, ← hyp', Fix.rec_eq]