Telescope infrastructure

This sets up the telescope infrastructure: cbn-based reduction in the proof mode (also used for maybe-wand which is kind of a testbed), and telescopic quantifiers for BIs including proof mode support.

To see this in full action, have a look at the ci/ralf/atomic branch, the logically atomic stack at iris-examples and iris-atomic ported to the new atomic triples.