This implements a proposal we discussed at the workshop: make the BI connectives we have in stdpp_scope (i.e., on
Prop level) be notation for
bi_emp_valid rather than
bi_entails. This has the advantage that we never implicitly have a
bi_entails somewhere in the middle of a formula. The exact location of
bi_entails is relevant when using
rewrite (and @gmalecha's automation); not being able to see where the turnstile is is quite confusing in those contexts.
The most painful part of this is big_op because we cannot use the proofmode there yet. The lemmas in HeapLang's proofmode.v are also outside the proofmode and I am not quite sure why. Some base_logic/lib files have some lemmas proved outside the proofmode but I don't think there is a good reason for that -- they just happen to match some of the
own lemmas exactly, so this was a bit shorter.