{C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {X : C} → {motive : P.Is X → Sort u_1} → ((prop : P X) → motive ⋯) → (t : P.Is X) → motive t