fix `head_stuck`

See merge request FP/iris-coq!144

  Also, remove the inconsistency that `wp_expr_eval` succeeds on a goal
  that is not a WP.

This reverts commit 45162e5a.
We have to wait until ssreflect makes an 8.8-compatible release.

gmultiset RA

See merge request FP/iris-coq!138

The closing view shift's LHS mask is now universally quantified, which
makes it easier to execute the closing view shift.

This is a substitute for !136.