{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {motive : CategoryTheory.Oplax.LaxTrans F G → Sort u} →
            (t : CategoryTheory.Oplax.LaxTrans F G) →
              ((app : (a : B) → F.obj a ⟶ G.obj a) →
                  (naturality :
                      {a b : B} →
                        (f : a ⟶ b) →
                          CategoryTheory.CategoryStruct.comp (app a) (G.map f) ⟶
                            CategoryTheory.CategoryStruct.comp (F.map f) (app b)) →
                    (naturality_naturality :
                        ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                          CategoryTheory.CategoryStruct.comp (naturality f)
                              (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)) (naturality g)) →
                      (naturality_id :
                          ∀ (a : B),
                            CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a))
                                (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a)) =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))
                                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).hom
                                  (CategoryTheory.Bicategory.leftUnitor (app a)).inv)) →
                        (naturality_comp :
                            ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                              CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g))
                                  (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c)) =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g))
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).inv
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                                      (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).hom
                                        (CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                                          (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).inv))))) →
                          motive
                            { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
                              naturality_id := naturality_id, naturality_comp := naturality_comp }) →
                motive t