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.