{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            {motive : CategoryTheory.Oplax.StrongTrans.Modification η θ → Sort u} →
              (t : CategoryTheory.Oplax.StrongTrans.Modification η θ) →
                ((app : (a : B) → η.app a ⟶ θ.app a) →
                    (naturality :
                        ∀ {a b : B} (f : a ⟶ b),
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
                              (θ.naturality f).hom =
                            CategoryTheory.CategoryStruct.comp (η.naturality f).hom
                              (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f))) →
                      motive { app := app, naturality := naturality }) →
                  motive t