Iris-internal solve_proper
We have some cases where a variant of solve_proper
that works inside the logic would be really useful:
- When using the fixed point of a monotone function (e.g., total WP).
- For showing co(ntra)variance of types in lambdaRust