restricted cases

Stream: lean4

[Robert Maxton]

I don't suppose there's any chance https://github.com/leanprover/lean4/issues/3212 can be extended to cases any time soon? I have a very similar issue where my cases_eliminator comes out of a quotient type, so requires a soundness side-condition that doesn't conclude in motive _; I can't use induction because my use case almost always has non-atomic parameters in the type of the scrutinee.