{𝒮 : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} →
          {P : Sort u} →
            {toNatTrans : CategoryTheory.NatTrans F.toFunctor G.toFunctor} →
              {isHomLift' :
                  autoParam
                    (∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans.app a))
                    CategoryTheory.BasedNatTrans.isHomLift'._autoParam} →
                {toNatTrans' : CategoryTheory.NatTrans F.toFunctor G.toFunctor} →
                  {isHomLift'' :
                      autoParam
                        (∀ (a : 𝒳.obj),
                          𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans'.app a))
                        CategoryTheory.BasedNatTrans.isHomLift'._autoParam} →
                    { toNatTrans := toNatTrans, isHomLift' := isHomLift' } =
                        { toNatTrans := toNatTrans', isHomLift' := isHomLift'' } →
                      (toNatTrans ≍ toNatTrans' → P) → P