∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X₁ : C₁) (X₂ : C₂)
  (X₃ : C₃),
  (((CategoryTheory.Functor.currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ =
    CategoryTheory.CategoryStruct.id
      (((((CategoryTheory.Functor.currying₃.functor.comp CategoryTheory.Functor.currying₃.inverse).obj F).obj X₁).obj
            X₂).obj
        X₃)