∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {ι : Type u_3} {S : C} {X : ι → C}
  (f : (i : ι) → X i ⟶ S) (ι' α : Type (max u_2 u_1)) (incl : ι' ⊕ α → ι)
  (motive :
    (T : C) → (u : T ⟶ S) → (u ∈ CategoryTheory.Presieve.ofArrows (fun i => X (incl i)) fun i => f (incl i)) → Prop)
  (T : C) (u : T ⟶ S) (x : u ∈ CategoryTheory.Presieve.ofArrows (fun i => X (incl i)) fun i => f (incl i)),
  (∀ (p : ι' ⊕ α), motive (X (incl p)) (f (incl p)) ⋯) → motive T u x