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

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.

As reported by @jjourdan: framing now no longer back tracks on whether
to strip laters or not. When framing below a later, we now only make it
strip laters of the head of the frame.

The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

Revert "Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type."

This reverts commit fa897ff5.

The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

Fixed by stdpp 93b4ec70e13a573a9055a5bf1269f5885e18e843.

We now use the `Maybe` prefix as also used for `Frame`: it indicates
whether progress has been made by stripping of a later or not.

We already supported framing under wands.

For example, framing `P` in `(P ∨ Q) ∗ R` now succeeds and turns the goal into `R`.

This partially solves #112.

This is to make sure that e.g. `//` in `iEval (rewrite .. // ..)` does
not immediately close the goal by reflexivity.

This should fix iris-examples.