∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} {α β : F ⟶ G} (h : α = β)
  (X : CategoryTheory.Endofunctor.Algebra G),
  ((CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h).hom.app X).f = CategoryTheory.CategoryStruct.id X.a