diff --git a/README.md b/README.md
index 4d336d3e3f48f08fb963cef728779c1a3b3f0867..bb35b8274154d10963fdd8f8612cb9233c48d163 100644
--- a/README.md
+++ b/README.md
@@ -137,8 +137,9 @@ Getting along with Iris in Coq:
 
 * Iris proof patterns and conventions are documented in the
   [proof guide](docs/proof_guide.md).
-* Various notions of equality in Iris and their Coq interface are described in the [equality
-  docs](docs/equalities.md).
+* Various notions of equality and logical entailment in Iris and their Coq
+  interface are described in the
+  [equality docs](docs/equalities_and_entailments.md).
 * The Iris tactics are described in the
   [the Iris Proof Mode (IPM) / MoSeL documentation](docs/proof_mode.md) as well as the
   [HeapLang documentation](docs/heap_lang.md).
diff --git a/docs/equalities.md b/docs/equalities.md
deleted file mode 100644
index c24dc23249ab9de0a66eff58e7c52974ec6ec370..0000000000000000000000000000000000000000
--- a/docs/equalities.md
+++ /dev/null
@@ -1,151 +0,0 @@
-# Equalities in Iris
-
-Using Iris involves dealing with a few subtly different equivalence and equality
-relations, especially among propositions.
-This document summarizes these relations and the subtle distinctions among them.
-This is not a general introduction to Iris: instead, we discuss the different
-Iris equalities and the interface to their Coq implementation. In particular, we
-discuss:
-- Equality from Iris metatheory vs Coq equality and setoid equivalence;
-- N-equivalence on OFEs;
-- Iris internal equality;
-- Iris entailment and bi-entailment.
-
-## Leibniz equality and setoids
-
-First off, in the metalogic (Coq) we have both the usual propositional (or
-Leibniz) equality `=`, and setoid equality `equiv` / `≡` (defined in `stdpp`).
-Notations for metalogic connectives like `≡` are declared in Coq scope
-`stdpp_scope`, which is "open" by default.
-
-Setoid equality for a type `A` is defined by the instance of `Equiv A`; this
-allows defining quotient setoids. To deal with setoids, we use Coq's
-[generalized
-rewriting](https://coq.inria.fr/refman/addendum/generalized-rewriting.html)
-facilities.
-
-Setoid equality can coincide with Leibniz equality:
-- `equivL` defines a setoid equality coinciding with Leibniz equality.
-- Some types enjoy `LeibnizEquiv`, which makes `equiv` be equivalent to `eq`.
-
-Given setoids `A` and `B` and a function `f : A → B`, an instance `Proper ((≡)
-==> (≡)) f` declares that `f` respects setoid equality, as usual in Coq. Such
-instances enable rewriting with setoid equalities.
-
-Here, stdpp adds the following facilities:
-- `solve_proper` for automating proofs of `Proper` instances.
-- `f_equiv` generalizes `f_equal` to other relations; it will for instance turn
-  goal `R (f a) (f b)` into `R a b` given an appropriate `Proper` instance
-  (here, `Proper (R ==> R) f`).
-
-## Equivalences on OFEs
-
-On paper, OFEs involve two relations, equality "=" and distance "=_n". In Coq,
-equality "=" is formalized as setoid equality, written `≡` or `equiv`, as before;
-distance "=_n" is formalized as relation `dist n`, also written `≡{n}≡`.
-Tactics `solve_proper` and `f_equiv` also support distance.
-
-Some OFE constructors choose interesting equalities.
-- `discreteO` constructs discrete OFEs (where distance coincides with setoid equality).
-- `leibnizO` constructs discrete OFEs (like `discreteO`) but using `equivL`, so
-  that both distance and setoid equality coincide with Leibniz equality.
-
-Given OFEs `A` and `B`, non-expansive functions from `A` to `B` are functions
-`f : A → B` with a proof of `NonExpansive f` (that is, `(∀ n, Proper (dist n
-==> dist n) f)`). The two can be packaged together via `A -n> B`.
-
-Non-expansive functions from Leibniz OFEs can be given type `A -d> B` instead of
-`leibnizO A -n> B`; this spares the need for bundled `NonExpansive` instances.
-Moreover, `discreteO A -n> B` is isomorphic to `f : A -d> B` plus an instance
-for `∀ n, Proper ((≡) ==> (≡{ n }≡)) f`. However, in the second case the
-`Proper` instance can be omitted for proof convenience unless actively used.
-
-In both OFE function spaces (`A -n> B` and `A -d> B`), setoid equality is
-defined to be pointwise equality, so that functional extensionality holds for `≡`.
-
-## Inside the Iris logic
-
-Next, we introduce notions internal to the Iris logic. Such notions often
-overload symbols used for external notions; however, those overloaded notations
-are declared in scope `bi_scope`; when writing `(P)%I`, notations in `P` are
-resolved in `bi_scope` in preference over `stdpp_scope`.
-We also use `bi_scope` for the arguments of all variants of Iris entailments.
-
-The Iris logic has an internal concept of equality. If `a` and `b` are Iris
-terms of type `A`, then their internal equality is written (on paper) "a =_A b";
-in Coq, that's written `a ≡ b` (notation for `sbi_internal_eq` in scope `bi_scope`).
-
-As shown in the Iris appendix, an internal equality `a ≡ b` is interpreted using
-OFE distance. Many types have `_equivI` lemmas characterizing internal
-equality on them. For instance, if `f, g : A -d> B`, lemma
-`discrete_fun_equivI` shows that `f ≡ g` is equivalent to `∀ x, f x ≡ g x`.
-Typically, each `_equivI` lemma for type `T` lifts to internal equality on
-`T` properties of the distance on `T`.
-
-## Relations among Iris propositions
-
-In this section, we discuss relations among internal propositions.
-Even though some of these notes generalize to all internal logics (other
-`sbi`s), we focus on Iris propositions (`iProp Σ`), to discuss both their proof
-theory and their model.
-As Iris propositions form a separation logic, we assume some familiarity with
-separation logics, connectives such as `-∗`, `∗`, `emp` and `→`, and the idea
-that propositions in separation logics are interpreted with predicates over
-resources (see for instance Sec. 2.1 of the MoSEL paper).
-
-In the metalogic, Iris defines the entailment relation between uniform
-predicates: intuitively, `P` entails `Q` (written `P ⊢ Q`) means that `P` implies
-`Q` on _every_ resource (for details see Iris appendix [Sec. 6]).
-Entailment `P ⊢ Q` is distinct from the magic wand, `(P -∗ Q)%I`, but
-equivalent, as `P ⊢ Q` is equivalent to `emp ⊢ P -∗ Q` (per Iris lemmas
-`entails_wand` and `wand_entails`).
-Notation `P ⊢ Q` is declared in `stdpp_scope`, but takes arguments in
-`bi_scope`, so that we can write conveniently `P ⊢ Q -∗ R` in `stdpp_scope`.
-For additional convenience, `P ⊢ Q` can also be written `P -∗ Q` in
-`stdpp_scope`, so that we can write `P -∗ Q -∗ R` instead of `P ⊢ Q -∗ R` or of
-the equivalent `emp ⊢ P -∗ Q -∗ R`.
-Using entailment, Iris defines an implicit coercion `bi_emp_valid`, mapping any
-Iris propositions `P` into the Coq propositions `emp ⊢ P`.
-
-On paper, uniform predicates are defined by quotienting by an equivalence
-relation ([Iris appendix, Sec. 3.3]); that relation is used in Coq as setoid
-equivalence. That relation is also equivalent to bi-entailment (or entailment in
-both directions), per lemma `equiv_spec`:
-```coq
-Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
-```
-
-Hence, setoid equality `≡` on propositions is also written `⊣⊢`. For instance,
-our earlier lemma `discrete_fun_equivI` is stated using `⊣⊢`:
-
-```coq
-Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) :
-  f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-```
-
-Inside the logic, we can use internal equality `≡` (in `bi_scope`), which
-translates to distance as usual. Here is a pitfall: internal equality `≡` is in
-general strictly stronger than `∗-∗`, because `Q1 ≡ Q2` means that `Q1` and `Q2`
-are equivalent _independently of the available resources_.
-- When proving `P -∗ Q1 ∗-∗ Q2`, we can use `P` to show that `Q1` and `Q2` are
-  equivalent.
-- Instead, to prove `P -∗ Q1 ≡ Q2`, we cannot use `P` unless it's a plain
-  proposition (so, one that holds on the empty resource). Crucially, pure
-  propositions `⌜ φ ⌝` are plain.
-
-We can explain internal equality using the Iris plainly modality:
-```coq
-Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
-```
-Looking at the Iris semantics for the plainly modality, to prove internal equality
-`P ≡ Q`, we must prove that `P` and `Q` are equivalent _without any resources
-available_.
-
-Last, metalevel propositions `φ : Prop` can be embedded as pure Iris
-propositions `⌜ φ ⌝`, and this allows embedding equalities from the metalogic.
-For instance, `⌜ a1 = a2 ⌝` can be useful for making some proofs more
-convenient, as Leibniz equality is the strongest equivalence available, is
-respected by all Coq functions, and can be used for rewriting in the absence of
-`Proper` instances. On the other hand, on-paper Iris does not allow writing
-`⌜ a1 = a2 ⌝`, only `⌜ a1 ≡ a2 ⌝`, unless setoid equality and Leibniz equality
-coincide.
diff --git a/docs/equalities_and_entailments.md b/docs/equalities_and_entailments.md
new file mode 100644
index 0000000000000000000000000000000000000000..201f0db9faea84b1ff036c3be074ea80ffc3f617
--- /dev/null
+++ b/docs/equalities_and_entailments.md
@@ -0,0 +1,151 @@
+# Equalities in Iris
+
+Using Iris involves dealing with a few subtly different equivalence and equality
+relations, especially among propositions.
+This document summarizes these relations and the subtle distinctions among them.
+This is not a general introduction to Iris: instead, we discuss the different
+Iris equalities and the interface to their Coq implementation. In particular, we
+discuss:
+- Equality ("=") in the *on-paper* Iris metatheory
+- Coq equality (`=`) and setoid equivalence (`≡`);
+- N-equivalence on OFEs (`≡{n}≡`);
+- Iris internal equality (`≡` in `bi_scope`);
+- Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
+
+We use `code font` for Coq notation and "quotes" for paper notation.
+
+## Leibniz equality and setoids
+
+First off, in the metalogic (Coq) we have both the usual propositional (or
+Leibniz) equality `=`, and setoid equality `equiv` / `≡` (defined in `stdpp`).
+Both of these are metalogic connectives from the perspective of Iris, and as
+such are declared in Coq scope `stdpp_scope`.
+
+Setoid equality for a type `A` is defined by the instance of `Equiv A`; this
+allows defining quotient setoids. To deal with setoids, we use Coq's
+[generalized
+rewriting](https://coq.inria.fr/refman/addendum/generalized-rewriting.html)
+facilities.
+
+Setoid equality can coincide with Leibniz equality, which is reflected by the
+`LeibnizEquiv` typeclass. We say that types with this property are "Leibniz
+types". `equivL` provides a convenient way to define a setoid with Leibniz
+equality. The tactics `fold_leibniz` and `unfold_leibniz` can be used to
+automatically turn all equalities of Leibniz types into `≡` or `=`.
+
+Given setoids `A` and `B` and a function `f : A → B`, an instance `Proper ((≡)
+==> (≡)) f` declares that `f` respects setoid equality, as usual in Coq. Such
+instances enable rewriting with setoid equalities.
+
+Here, stdpp adds the following facilities:
+- `solve_proper` for automating proofs of `Proper` instances.
+- `f_equiv` generalizes `f_equal` to setoids (and indeed arbitrary relations
+  registered with Coq's generalized rewriting). It will for instance turn the
+  goal `f a ≡ f b` into `a ≡ b` given an appropriate `Proper` instance (here,
+  `Proper ((≡) ==> (≡)) f`).
+
+## Equivalences on OFEs
+
+On paper, OFEs involve two relations, equality "=" and distance "=_n". In Coq,
+equality "=" is formalized as setoid equality, written `≡` or `equiv`, as before;
+distance "=_n" is formalized as relation `dist n`, also written `≡{n}≡`.
+Tactics `solve_proper` and `f_equiv` also support distance. There is no
+correspondence to Coq's `=` on paper.
+
+Some OFE constructors choose interesting equalities.
+- `discreteO` constructs discrete OFEs (where distance coincides with setoid equality).
+- `leibnizO` constructs discrete OFEs (like `discreteO`) but using `equivL`, so
+  that both distance and setoid equality coincide with Leibniz equality. This
+  should only be used for types that do not have a setoid equality registered.
+
+Given OFEs `A` and `B`, non-expansive functions from `A` to `B` are functions
+`f : A → B` with a proof of `NonExpansive f` (which is notation for `∀ n, Proper
+(dist n ==> dist n) f`).
+
+The type `A -n> B` packages a function with a non-expansiveness proof. This is
+useful because `A -n> B` is itself an OFE, but should be avoided whenever
+possible as it requires the caller to specifically package up function and proof
+(which works particularly badly for lambda expressions).
+
+When an OFE structure on a function type is required but the domain is discrete,
+one can use the type `A -d> B`.  This has the advantage of not bundling any
+proofs, i.e., this is notation for a plain Coq function type. See the
+`discrete_fun` documentation in `iris.algebra.ofe` for further details.
+
+In both OFE function spaces (`A -n> B` and `A -d> B`), setoid equality is
+defined to be pointwise equality, so that functional extensionality holds for `≡`.
+
+## Inside the Iris logic
+
+Next, we introduce notions internal to the Iris logic. Such notions often
+overload symbols used for external notions; however, those overloaded notations
+are declared in scope `bi_scope`. When writing `(P)%I`, notations in `P` are
+resolved in `bi_scope`; this is done implicitly for the arguments of all
+variants of Iris entailments.
+
+The Iris logic has an internal concept of equality: if `a` and `b` are Iris
+terms of type `A`, then their internal equality is written (on paper) "a =_A b";
+in Coq, that's written `(a ≡ b)%I` (notation for `bi_internal_eq` in scope
+`bi_scope`). The type annotation on paper only exist for the purpose of being
+fully explicit; it can be omitted as is common for other notions of equality and
+it is inferred in Coq.
+
+As shown in the Iris appendix, an internal equality `(a ≡ b)%I` is interpreted using
+OFE distance at the current step-index. Many types have `_equivI` lemmas
+characterizing internal equality on them. For instance, if `f, g : A -d> B`,
+lemma `discrete_fun_equivI` shows that `(f ≡ g)%I` is equivalent to
+`(∀ x, f x ≡ g x)%I`.
+
+An alternative to internal equality is to embed Coq equality into the Iris logic
+using `⌜ _ ⌝%I`.  For discrete types, `(a ≡ b)%I` is equivalent to `⌜a ≡ b⌝%I`,
+and the latter can be moved into the Coq context, making proofs more convenient.
+For types with Leibniz equality, we can even equivalently write `⌜a = b⌝%I`, so
+no `Proper` is needed for rewriting.  Note that there is no on-paper equivalent
+to using these embedded Coq equalities for types that are not discrete/Leibniz.
+
+## Relations among Iris propositions
+
+In this section, we discuss relations among internal propositions, and in particular equality/equivalence of propositions themselves.
+Even though some of these notes generalize to all internal logics (other
+`bi`s), we focus on Iris propositions (`iProp`), to discuss both their proof
+theory and their model.
+As Iris propositions form a separation logic, we assume some familiarity with
+separation logics, connectives such as `-∗`, `∗`, `emp` and `→`, and the idea
+that propositions in separation logics are interpreted with predicates over
+resources (see for instance Sec. 2.1 of the MoSEL paper).
+
+In the metalogic, Iris defines the entailment relation between uniform
+predicates: intuitively, `P` entails `Q` (written `P ⊢ Q`) means that `P`
+implies `Q` on _every_ resource (for details see Iris appendix [Sec. 6]).
+Entailment `P ⊢ Q` is distinct from the magic wand, `(P -∗ Q)%I`: the former is
+a Coq-level statement of type `Prop`, the latter an Iris-level statement of type
+`iProp`.  However, the two are closely related: `P ⊢ Q` is equivalent to `emp ⊢
+P -∗ Q` (per Iris lemmas `entails_wand` and `wand_entails`).  Iris also defines
+a "unary" form of entailment, `⊢ P`, which is short for `emp ⊢ P`.
+We can also use bi-entailment `P ⊣⊢ Q` to express that both `P ⊢ Q` and `Q ⊢ P` gold.
+
+On paper, uniform predicates are defined by quotienting by an equivalence
+relation ([Iris appendix, Sec. 3.3]); in Coq, that relation is chosen as the
+setoid equivalent for the type of Iris propositions.
+This equivalence is actually equivalent to bi-entailment, per lemma `equiv_spec`:
+```coq
+Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+```
+Relying on this equivalence, bi-entailment `P ⊣⊢ Q` is defined as notation for `≡`.
+
+## Internal equality of Iris propositions
+
+Inside the logic, we can use internal equality `(≡)%I` on any type, including
+propositions themselves.  However, there is a pitfall here: internal equality
+`≡` is in general strictly stronger than `∗-∗` (the bidirectional version of the
+magic wand), because `Q1 ≡ Q2` means that `Q1` and `Q2` are equivalent
+_independently of the available resources_.  The two notions of internal
+equivalence and equality of propositions are related by the following law of
+propositional extensionality:
+```coq
+Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
+```
+This uses the plainly modality `â– ` to reflect that equality corresponds to
+equivalence without any resources available: `â–  R` says that `R` holds
+independent of any resources that we might own (but still taking into account
+the current step-index).