Is your feature request related to a problem?

I am trying to write a tactic fold_match : constr -> constr whose specification is that when the constr it gets is headed by a match / case, if there is a way to instantiate a registered scheme / elimination principle to unfold to the specified constant, then fold_match c is convertible with c and uses the registered elimination principle. I have a version that works fine for non-recursive inductives (by leveraging induction), but I don't see a way to get my hands on things that come from, e.g., Scheme Minimality for list Sort Type.

Proposed solution

I would like to be able to perform lookup_schemes [Induction|Minimality|Equality] ident sort and get a list of scheme constants / an optional scheme info. Or there could be separate lookup_scheme_induction ident sort, lookup_scheme_minimality ident sort, lookup_scheme_equality ident.

Alternative solutions

I'd also be happy with a variant of destruct that used registered non-dependent schemes instead of a raw match

Additional context

No response