{P : Type u_1} →
  [inst : Preorder P] →
    {I : Order.Ideal P} →
      {motive : I.IsPrime → Sort u} →
        (t : I.IsPrime) → ([toIsProper : I.IsProper] → (compl_filter : Order.IsPFilter (↑I)ᶜ) → motive ⋯) → motive t