∀ {C : Type u_3} {D : Type u_5} [inst : CategoryTheory.Category.{u_6, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_5} D] (F : CategoryTheory.Functor C D) {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{u_1, u_2} J] (G : CategoryTheory.Over F)
  (motive : CategoryTheory.ObjectProperty.limitsOfShape (fun f => CategoryTheory.NatTrans.Equifibered f.hom) J G → Prop)
  (x : CategoryTheory.ObjectProperty.limitsOfShape (fun f => CategoryTheory.NatTrans.Equifibered f.hom) J G),
  (∀ (c : CategoryTheory.Functor J (CategoryTheory.Over F)) (α : (CategoryTheory.Functor.const J).obj G ⟶ c)
      (hc : CategoryTheory.Limits.IsLimit { pt := G, π := α })
      (H : ∀ (j : J), CategoryTheory.NatTrans.Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom),
      motive ⋯) →
    motive x