{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {motive : F.IsRepresentable → Sort u} →
        (t : F.IsRepresentable) → ((has_representation : ∃ Y, Nonempty (F.RepresentableBy Y)) → motive ⋯) → motive t