Sublist elimination to Type

Stream: Is there code for X?

[Wrenna Robson]

So one can define the following.

def Sublist.recOnType [BEq α] [LawfulBEq α] {motive : (s t : List α) → s <+ t → Type*}
    (slnil : motive [] [] .slnil) (cons : ∀ {s t a h}, motive s t h → motive s (a :: t) (.cons _ h))
    (cons₂ : ∀ {s t a h}, motive s t h → motive (a :: s) (a :: t) (.cons₂ _ h)) :
    {s t : List α} → (h : s <+ t) → motive s t h
  | [], [], _ => slnil
  | x :: s, [], h => (cons_ne_nil _ _ (eq_nil_of_sublist_nil h)).elim
  | [], y :: t, _ => cons <| (nil_sublist _).recOnType slnil cons cons₂
  | x :: s, y :: t, h => match hxy : x == y with
    | true => eq_of_beq hxy ▸ cons₂ (h.of_cons_cons.recOnType slnil cons cons₂)
    | false => cons <| (of_cons_of_ne (ne_of_beq_false hxy) h).recOnType slnil cons cons₂

This basically says that as long as you have a lawful BEq (or DecidableEq if you prefer) you can eliminate the predicate Sublist s t not just to Prop (which is produced by default) but in fact to Type* (indeed to Sort, but here I've used Type to avoid confusion with the existing eliminator).

Now it seems to me quite natural to want to do this in certain places, and indeed to produce something similar for other predicates like Perm, Subperm, or Subset. Do we do this anywhere already? Is there a good reason why not?