∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] ⦃X : C⦄ (S : CategoryTheory.Presieve X)
  (motive :
    S ∈
        {S |
          ∃ X_1 f, (S = CategoryTheory.Presieve.ofArrows (fun x => X_1) fun x => f) ∧ CategoryTheory.EffectiveEpi f} →
      Prop)
  (h :
    S ∈
      {S | ∃ X_1 f, (S = CategoryTheory.Presieve.ofArrows (fun x => X_1) fun x => f) ∧ CategoryTheory.EffectiveEpi f}),
  (∀ (Z : C) (π : Z ⟶ X) (hπ : S = CategoryTheory.Presieve.ofArrows (fun x => Z) fun x => π)
      (h_epi : CategoryTheory.EffectiveEpi π), motive ⋯) →
    motive h