{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η : F ⟶ G} →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (η.app a) (G.map f) ≅
                      CategoryTheory.CategoryStruct.comp (F.map f) (η.app b)) →
              autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
                  CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom._autoParam →
                CategoryTheory.Lax.LaxTrans.StrongCore η