∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_5, u_4} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type u_1} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S) (motive : Nonempty (F.toDescentData f).FullyFaithful → Prop)
  (x : Nonempty (F.toDescentData f).FullyFaithful), (∀ (h : (F.toDescentData f).FullyFaithful), motive ⋯) → motive x