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