{α : Type u_1} →
  [inst : LE α] →
    {motive : LowerSet α → Sort u} →
      (t : LowerSet α) →
        ((carrier : Set α) → (lower' : IsLowerSet carrier) → motive { carrier := carrier, lower' := lower' }) → motive t