∀ {X Y : CategoryTheory.Cat} {X_1 Y_1 : X ⟶ Y} (η : X_1 ⟶ Y_1),
  CategoryTheory.NatTrans.toCatHom₂
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.CategoryStruct.id X_1.toFunctor)).toNatTrans η.toNatTrans) =
    CategoryTheory.NatTrans.toCatHom₂ η.toNatTrans