Better handling of `let` bindings in proof mode

Closes #520

See merge request iris/iris!921

This fixes the second bug in issue #520.

These should either be `simpl`ed or introduced into the Coq context.
Fixes the first bug in issue #520.

Thanks, Johannes!

make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)

See merge request iris/iris!791

add locality annotation to all Typeclasses Opaque/Transparent

See merge request iris/iris!918

use more primitive projections in cmra.v

See merge request iris/iris!919

spygame and time-credits don't send nightly build results to the shared iris-dev; also don't run them in rev-dep checks

Make projections of BI operational type classes `Typeclasses Opaque`.

See merge request iris/iris!914

Update prelude file to use new ssreflect file from std++.

See merge request iris/iris!917

Bump stdpp

See merge request iris/iris!915

drop support for Coq 8.14

See merge request iris/iris!908