∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {B : C} {α : Type u_3} (X : α → C)
  (π : (a : α) → X a ⟶ B) (motive : (CategoryTheory.Sieve.generateFamily X π).arrows.category → Prop)
  (h : (CategoryTheory.Sieve.generateFamily X π).arrows.category),
  (∀ (T : CategoryTheory.Over B) (a : α) (g : T.left ⟶ X a) (hT : CategoryTheory.CategoryStruct.comp g (π a) = T.hom),
      motive { obj := T, property := ⋯ }) →
    motive h