diff --git a/CHANGELOG.md b/CHANGELOG.md
index 076e6a025b459cf12b9f0d3559ec90e18898e88c..83c26d5dd4617e780143600e3b59f2a4eba4310f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -47,13 +47,26 @@ Coq 8.13 is no longer supported.
 * Add compatibility lemmas for `big_sepL <-> big_sepL2`, `big_sepM <-> big_sepM2`
   with list/maps of pairs; and `big_sepM <-> big_sepL` via `list_to_map` and
   `map_to_list`. (by Dorian Lesbre).
-- Make `persistently_True` a bi-entailment; this changes the default `rewrite`
+* Make `persistently_True` a bi-entailment; this changes the default `rewrite`
   direction.
-- Make `BiLaterContractive` a class instead of a notation.
-- Make projections of `Bupd`/`Fupd`/`InternalEq`/`Plainly` operational type
+* Make `BiLaterContractive` a class instead of a notation.
+* Make projections of `Bupd`/`Fupd`/`InternalEq`/`Plainly` operational type
   classes `Typeclasses Opaque`.
-- Make BI relations (`bi_rtc`, `bi_tc`, `bi_nsteps`) typeclasses opaque (they
+* Make BI relations (`bi_rtc`, `bi_tc`, `bi_nsteps`) typeclasses opaque (they
   were accidentally transparent).
+* Make the `P -∗ Q` notation in stdpp_scope (i.e., outside of bi_scope) a
+  shorthand for `⊢ P -∗ Q` rather than `P ⊢ Q`. This means that any BI notation
+  used in stdpp_scope will be sugar for adding a leading `⊢` (`bi_emp_valid`).
+  It also means that `apply` becomes sensitive to the difference between `P ⊢ Q`
+  and `P -∗ Q`, and `rewrite` will only work with lemmas that are explicitly
+  written using `⊢`.
+  When a proof breaks, there are generally 3 options:
+  - Try to find the `-∗` that should be turned into a `⊢` so that things work
+    like before.
+  - Adjust the proof to use proof mode tactics rather than Coq tactics (in
+    particular, replace `apply` by `iApply`).
+  - Add some `apply bi.entails_wand`/`apply bi.wand_entails` to 'convert'
+    between the old and new way of interpreting `P -∗ Q`.
 
 **Changes in `proofmode`:**
 
diff --git a/docs/style_guide.md b/docs/style_guide.md
index 22a947d24ae48d682e1655e1e85cb3bdd43afb73..370426bcede81e2635bb4f39a24e54bd8dcd8441 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -210,6 +210,20 @@ theories/base_logic/lib is for constructions in the base logic (using own)
 * Parameter order is usually from more higher-order to less higher-order (types, functions, plain values), and otherwise follows the order in which variables appear in the lemma statement.
 * In new lemmas, arguments should be marked as implicit when they can be inferred by unification in all intended usage scenarios. (If an argument can *sometimes* be inferred, we do not have a clear guideline yet -- consider on a case-by-case basis, for now.)
 
+## Lemma statements
+
+### Iris lemmas: `-∗` vs `⊢`
+
+* For low-level lemmas, in particular if there is a high likelyhood someone would want to rewrite with it / use them in non-proofmode goals (e.g. modality intro rules), use `⊢`
+  * `P ⊢ |==£> P`
+  * `(|==£> |==£> P) ⊢ |==£> P`
+  * `▷ own γ a ⊢ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b)`
+  * `(P -∗ Q) i ⊢ (P i -∗ Q i)`
+* If a lemma is a Coq implication of Iris entailments (where the entailments are visible, not hidden behind e.g. `Persistent`), then use `⊢`
+  * `(P1 ⊢ P2) → recv l P1 ⊢ recv l P2`
+* Else use -∗
+  * `a1 ⋅ a2 ~~> a' → own γ a1 -∗ own γ a2 ==∗ own γ a'` (curried and hence not rewrite-friendly)
+
 ## Metavariables
 **TODO:** move these to the right place
 
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 59546f2c468b1d1f8ca8d5425e7b4c557a4b2041..2cb34dfceb0b70ba50fcbdfd110a3c136c370bea 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -136,7 +136,7 @@ Qed.
   these cannot be used for anything. They are merely provided to enable making
   the adequacy proof generic in whether later credits are used. *)
 Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
-  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢ |={E1,E2}=> P) → ⊢ P.
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={E1,E2}=∗ P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
   (* We don't actually want any credits, but we need the [lcGS]. *)
@@ -149,7 +149,7 @@ Proof.
 Qed.
 
 Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
-  (∀ `{Hinv: !invGS_gen HasLc Σ}, £ n ⊢@{iPropI Σ} |={E1,E2}=> P) → ⊢ P.
+  (∀ `{Hinv: !invGS_gen HasLc Σ}, £ n ={E1,E2}=∗ P) → ⊢ P.
 Proof.
   iIntros (Hfupd). eapply (lc_soundness (S n)); first done.
   intros Hc. rewrite lc_succ.
@@ -181,7 +181,7 @@ Qed.
 (** [step_fupdN] soundness lemmas *)
 
 Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
-  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n P) →
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={⊤,∅}=∗ |={∅}▷=>^n P) →
   ⊢ P.
 Proof.
   intros Hiter.
@@ -195,7 +195,7 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
-  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n P) →
+  (∀ `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={⊤}[∅]▷=∗^n P) →
   ⊢ P.
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv.
@@ -207,7 +207,7 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
-  (∀ `{Hinv: !invGS_gen HasLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n P) →
+  (∀ `{Hinv: !invGS_gen HasLc Σ}, £ m ={⊤,∅}=∗ |={∅}▷=>^n P) →
   ⊢ P.
 Proof.
   intros Hiter.
@@ -223,7 +223,7 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
-  (∀ `{Hinv: !invGS_gen hlc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n P) →
+  (∀ `{Hinv: !invGS_gen hlc Σ}, £ m ={⊤}[∅]▷=∗^n P) →
   ⊢ P.
 Proof.
   intros Hiter.