For half of #231.

make pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbn

All those for `big_sepL` that hold.

* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics
* use reduction-controlled `pm_default` for proofmode accessors

The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.

If the accessor introduces a binder, the first Coq-level intro pattern of `iInv`
is used for that binder unless the type of the binder is unit, in which case
`iInv` removes it completely.  Binders on the closing view shift are not (yet)
supported as they are harder to smoothly eliminate in the unit case.

New IntoAcc typeclass to decouple creating and elliminating accessors; ElimInv supports both with and without Hclose

Fixes #156

Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context.

Fixes #177