Better syntax for pm_terms

[markusdemedeiros]

Proofmode terms currently use Iris syntax, which specializes terms using a clunky with and $! for Iris and Lean level variables separately.

Is a cleaner syntax possible?

[Shreyas4991]

You could just borrow the cases/rcases syntax. It comes with nice code actions.