{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          {motive : CategoryTheory.NatTrans F G → Sort u} →
            (t : CategoryTheory.NatTrans F G) →
              ((app : (X : C) → F.obj X ⟶ G.obj X) →
                  (naturality :
                      ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
                        CategoryTheory.CategoryStruct.comp (F.map f) (app Y) =
                          CategoryTheory.CategoryStruct.comp (app X) (G.map f)) →
                    motive { app := app, naturality := naturality }) →
                motive t