∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (f f_1 : A₀.a ⟶ A₁.a) (e_f : f = f_1)
  (h : CategoryTheory.CategoryStruct.comp (F.map f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f),
  { f := f, h := h } = { f := f_1, h := ⋯ }