∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {D : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_5, u_3} D] {E : Type u_4} [inst_2 : CategoryTheory.Category.{u_6, u_4} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y Z : CategoryTheory.ThinSkeleton C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.ThinSkeleton.map₂NatTrans F (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ThinSkeleton.map₂NatTrans F f)
      (CategoryTheory.ThinSkeleton.map₂NatTrans F g)