Commit 2024-07-24 13:07 bbbb785d

chore: address elab_as_elim workarounds (#15091) There were a number of places that eliminator elaboration was suppressed using the (motive := _) trick to be used in conjuction with apply, but it's generally clearer to use induction, refine, or, sometimes, rintro (for Quot).