{α : Type u_1} →
  [inst : LE α] →
    {P : α → Prop} →
      {motive : RelLowerSet P → Sort u} →
        ((carrier : Set α) →
            (isRelLowerSet' : IsRelLowerSet carrier P) →
              motive { carrier := carrier, isRelLowerSet' := isRelLowerSet' }) →
          (t : RelLowerSet P) → motive t