∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} (S : CategoryTheory.Sieve X)
  (motive : S.arrows.category → Prop) (x : S.arrows.category),
  (∀ (f : C) (right : CategoryTheory.Discrete PUnit.{1})
      (hom : (CategoryTheory.Functor.id C).obj f ⟶ (CategoryTheory.Functor.fromPUnit X).obj right)
      (hf : S.arrows { left := f, right := right, hom := hom }.hom),
      motive { obj := { left := f, right := right, hom := hom }, property := hf }) →
    motive x