diff --git a/docs/heap_lang.md b/docs/heap_lang.md
index 1934fcb6b2263ee40a033a85a5cf3f17e91e504d..aeaa29915789fe36c82d9e2ea154ec38c6426a1d 100644
--- a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ -33,7 +33,7 @@ constructor).
 ## Notation
 
 Notation for writing HeapLang terms is defined in
-[`notation.v`](theories/heap_lang/notation.v).  There are two scopes, `%E` for
+[`notation.v`](../theories/heap_lang/notation.v).  There are two scopes, `%E` for
 expressions and `%V` for values.  For example, `(a, b)%E` is an expression pair
 and `(a, b)%V` a value pair.  The `e` of a `WP e {{ Q }}` is implicitly in `%E`
 scope.
diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 3195c63d2d83219f80aec5e8668480d03e197c62..cc1f820b3476f914b21499ba0089adbb1ccbdf57 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -16,241 +16,13 @@ In particular, when importing Iris, Stdpp and Coq stdlib modules, we
 recommend importing in the following order:
 - Coq
 - stdpp
+- iris.algebra
 - iris.bi
 - iris.proofmode
-- iris.algebra
 - iris.base_logic
 - iris.program_logic
 - iris.heap_lang
 
-## Combinators for functors
-
-In Iris, the type of propositions [iProp] is described by the solution to the
-recursive domain equation:
-
-```
-iProp ≅ uPred (F (iProp))
-```
-
-Here, `F` is a user-chosen locally contractive bifunctor from COFEs to unital
-Cameras (a step-indexed generalization of unital resource algebras). To make it
-convenient to construct such functors out of smaller pieces, we provide a number
-of abstractions:
-
-- [`cFunctor`](theories/algebra/ofe.v): bifunctors from COFEs to OFEs.
-- [`rFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to cameras.
-- [`urFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to unital
-  cameras.
-
-Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
-`urFunctorContractive` which describe the subset of the above functors that
-are contractive.
-
-To compose these functors, we provide a number of combinators, e.g.:
-
-- `constCF (A : ofeT) : cFunctor           := λ (B,B⁻), A `
-- `idCF : cFunctor                         := λ (B,B⁻), B`
-- `prodCF (F1 F2 : cFunctor) : cFunctor    := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
-- `ofe_morCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
-- `laterCF (F : cFunctor) : cFunctor       := λ (B,B⁻), later (F (B,B⁻))`
-- `agreeRF (F : cFunctor) : rFunctor       := λ (B,B⁻), agree (F (B,B⁻))`
-- `gmapURF K (F : rFunctor) : urFunctor    := λ (B,B⁻), gmap K (F (B,B⁻))`
-
-Using these combinators, one can easily construct bigger functors in point-free
-style, e.g:
-
-```
-F := gmapURF K (agreeRF (prodCF (constCF natC) (laterCF idCF)))
-```
-
-which effectively defines `F := λ (B,B⁻), gmap K (agree (nat * later B))`.
-
-Furthermore, for functors written using these combinators like the functor `F`
-above, Coq can automatically `urFunctorContractive F`.
-
-To make it a little bit more convenient to write down such functors, we make
-the constant functors (`constCF`, `constRF`, and `constURF`) a coercion, and
-provide the usual notation for products, etc. So the above functor can be
-written as follows (which is similar to the effective definition of `F` above):
-
-```
-F := gmapURF K (agreeRF (natC * ▶ ∙))
-```
-
-## Resource algebra management
-
-When using ghost state in Iris, you have to make sure that the resource algebras
-you need are actually available.  Every Iris proof is carried out using a
-universally quantified list `Σ: gFunctors` defining which resource algebras are
-available.  The `Σ` is the *global* list of resources that the entire proof can
-use.  We keep the `Σ` universally quantified to enable composition of proofs.
-
-You can think of this as a list of resource algebras, though in reality it is a
-list of locally contractive functors from COFEs to Cameras.  This list is used
-to define the parameter `F` of Iris mentioned in the previous section. The
-formal side of this is described in §7.4 of
-[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we
-describe the user-side Coq aspects of this approach.
-
-The assumptions that an Iris proof makes are collected in a type class called
-`somethingG`.  The most common kind of assumptions is `inG`, which says that a
-particular resource algebra is available for ghost state.  For example, in the
-[one-shot example](tests/one_shot.v):
-```
-Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
-```
-The `:>` means that the projection `one_shot_inG` is automatically registered as
-an instance for type-class resolution.  If you need several resource algebras,
-just add more `inG` fields.  If you are using another module as part of yours,
-add a field like `one_shot_other :> otherG Σ`.
-
-Having defined the type class, we need to provide a way to instantiate it.  This
-is an important step, as not every resource algebra can actually be used: if
-your resource algebra refers to `Σ`, the definition becomes recursive.  That is
-actually legal under some conditions (which is why the global list `Σ` contains
-functors and not just resource algebras), but for the purpose of this guide we
-will ignore that case.  We have to define a list that contains all the resource
-algebras we need:
-```
-Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
-```
-This time, there is no `Σ` in the context, so we cannot accidentally introduce a
-bad dependency.  If you are using another module as part of yours, add their
-`somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`.  (The
-`#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each
-other; together with a coercion from a single functor to a singleton list, this
-means lists can be nested arbitrarily.)
-
-Now we can define the one and only instance that our type class will ever need:
-```
-Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
-Proof. solve_inG. Qed.
-```
-The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
-global list `Σ`.  Typically, this should be the only assumption your instance
-needs, showing that the assumptions of the module (and all the modules it
-uses internally) can trivially be satisfied by picking the right `Σ`.
-
-Now you can add `one_shotG` as an assumption to all your module definitions and
-proofs.  We typically use a section for this:
-```
-Section proof.
-Context `{!heapG Σ, !one_shotG Σ}.
-```
-Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
-which are assumptions that every HeapLang proof makes (they are related to
-defining the `↦` connective as well as the basic Iris infrastructure for
-invariants and WP).  For this purpose, `heapG` contains not only assumptions
-about `Σ`, it also contains some ghost names to refer to particular ghost state
-(see "global ghost state instances" below).
-
-The backtick (`` ` ``) is used to make anonymous assumptions and to automatically
-generalize the `Σ`.  When adding assumptions with backtick, you should most of
-the time also add a `!` in front of every assumption.  If you do not then Coq
-will also automatically generalize all indices of type-classes that you are
-assuming.  This can easily lead to making more assumptions than you are aware
-of, and often it leads to duplicate assumptions which breaks type class
-resolutions.
-
-### Obtaining a closed proof
-
-To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
-`inG`, you have to assemble a list of functors of all the involved modules,
-and if your proof relies on some singleton (most do, at least indirectly; also
-see the next section), you have to call the respective initialization or
-adequacy lemma.  [For example](tests/one_shot.v):
-```
-Section client.
-  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
-
-  Lemma client_safe : WP client {{ _, True }}%I.
-  (* ... *)
-End client.
-
-(** Assemble all functors needed by the [client_safe] proof. *)
-Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
-
-(** Apply [heap_adequacy] with this list of all functors. *)
-Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
-```
-
-### Advanced topic: Ghost state singletons
-
-Some Iris modules involve a form of "global state".  For example, defining the
-`↦` for HeapLang involves a piece of ghost state that matches the current
-physical heap.  The `gname` of that ghost state must be picked once when the
-proof starts, and then globally known everywhere.  Hence it is added to
-`gen_heapG`, the type class for the generalized heap module:
-```
-Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
-  gen_heap_name : gname
-}.
-```
-
-Such modules always need some kind of "initialization" to create an instance
-of their type class.  For example, the initialization for `heapG` is happening
-as part of [`heap_adequacy`](theories/heap_lang/adequacy.v); this in turn uses
-the initialization lemma for `gen_heapG` from
-[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
-```
-Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
-  (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
-```
-These lemmas themselves only make assumptions the way normal modules (those
-without global state) do, which are typically collected in a `somethingPreG`
-type class (such as `gen_heapPreG`):
-```
-Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V))
-}.
-```
-Just like in the normal case, `somethingPreG` type classes have an `Instance`
-showing that a `subG` is enough to instantiate them:
-```
-Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
-  subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
-Proof. solve_inG. Qed.
-```
-The initialization lemma then shows that the `somethingPreG` type class is
-enough to create an instance of the main `somethingG` class *below a view
-shift*.  This is written with an existential quantifier in the lemma because the
-statement after the view shift (`gen_heap_ctx σ` in this case) depends on having
-an instance of `gen_heapG` in the context.
-
-Given that these global ghost state instances are singletons, they must be
-assumed explicitly everywhere.  Bundling `heapG` in a module type class like
-`one_shotG` would lose track of the fact that there exists just one `heapG`
-instance that is shared by everyone.
-
-### Advanced topic: Additional module assumptions
-
-Some modules need additional assumptions.  For example, the STS module is
-parameterized by an STS and assumes that the STS state space is inhabited:
-```
-Class stsG Σ (sts : stsT) := {
-  sts_inG :> inG Σ (stsR sts);
-  sts_inhabited :> Inhabited (sts.state sts);
-}.
-```
-In this rather exceptional case, the `Instance` for this class has more than
-just a `subG` assumption:
-```
-Instance subG_stsΣ Σ sts :
-  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
-```
-If users of this module follow the pattern described above, their own type class
-instance will check these additional assumption.  But this is one more reason
-why it is important for every module to have an instance for its `somethingG`:
-to make sure that it does not accidentally make more assumptions than it intends
-to.
-
-Another subtle detail here is that the `subG` assumption comes first in
-`subG_stsΣ`, i.e., it appears before the `Inhabited`.  This is important because
-otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
-type class search diverge.
-
 ## Canonical structures and type classes
 
 In Iris, we use both canonical structures and type classes, and some careful
@@ -278,15 +50,41 @@ avoided.
 ## Type class resolution control
 
 When you are writing a module that exports some Iris term for others to use
-(e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be
+(e.g., `join_handle` in the [spawn module](../theories/heap_lang/lib/spawn.v)), be
 sure to mark these terms as opaque for type class search at the *end* of your
 module (and outside any section):
-```
+```coq
 Typeclasses Opaque join_handle.
 ```
 This makes sure that the proof mode does not "look into" your definition when it
 is used by clients.
 
+## Library type class assumptions
+
+When a parameterized library needs to make some type class assumptions about its
+parameters, it is convenient to add those to the `libG` class that the library
+will likely need anyway (see the [resource algebra docs](resource_algebras.md)
+for further details on `libG` classes).  For example, the STS library is
+parameterized by an STS and assumes that the STS state space is inhabited:
+```coq
+Class stsG Σ (sts : stsT) := {
+  sts_inG :> inG Σ (stsR sts);
+  sts_inhabited :> Inhabited (sts.state sts);
+}.
+```
+In this case, the `Instance` for this `libG` class has more than just a `subG`
+assumption:
+```coq
+Instance subG_stsΣ Σ sts :
+  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
+Proof. solve_inG. Qed.
+```
+
+One subtle detail here is that the `subG` assumption comes first in
+`subG_stsΣ`, i.e., it appears before the `Inhabited`.  This is important because
+otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
+type class search diverge.
+
 ## Notations
 
 Notations starting with `(` or `{` should be left at their default level (`0`),
@@ -321,13 +119,12 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * j
 * k
 * l
-* m : iGst = ghost state
-* m* = prefix for option
+* m* = prefix for option ("maybe")
 * n
 * o
 * p
 * q
-* r : iRes = resources
+* r : iRes = (global) resources inside the Iris model
 * s = state (STSs)
 * s = stuckness bits
 * t
@@ -343,8 +140,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * A : Type, cmraT or ofeT
 * B : Type, cmraT or ofeT
 * C
-* D   
-* E : coPset = Viewshift masks
+* D
+* E : coPset = mask of fancy update or WP
 * F = a functor
 * G
 * H = hypotheses
@@ -362,7 +159,7 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * S : set state = state sets in STSs
 * T : set token = token sets in STSs
 * U
-* V : abstraction of value type in frame shift assertions
+* V
 * W
 * X : sets
 * Y : sets
@@ -370,14 +167,14 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 
 ### small greek letters
 
-* γ : gname
+* γ : gname = name of ghost state instance
 * σ : state = state of language
-* φ : interpretation of STS/Auth
+* φ : Prop = pure proposition embedded into uPred or iProp
 
 ### capital greek letters
 
-* Φ : general predicate (over uPred, iProp or Prop)
-* Ψ : general predicate (over uPred, iProp or Prop)
+* Φ : general predicate (in uPred, iProp or Prop)
+* Ψ : general predicate (in uPred, iProp or Prop)
 
 ## Naming conventions for algebraic classes
 
@@ -387,8 +184,8 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * R: cameras
 * UR: unital cameras or resources algebras
 * F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
-* G: global camera functor management (typeclass; see [proof\_guide.md](./proof_guide.md))
+* G: global camera functor management (typeclass; see the [resource algebra docs](resource_algebras.md))
 * I: bunched implication logic (of type `bi`)
 * SI: step-indexed bunched implication logic (of type `sbi`)
 * T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
-* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](./proof_guide.md))
+* Σ: global camera functor management (`gFunctors`; see the [resource algebra docs](resource_algebras.md))
diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
new file mode 100644
index 0000000000000000000000000000000000000000..ca3638f6f85149aba7fdbaa084bbe43e5dfe8574
--- /dev/null
+++ b/docs/resource_algebras.md
@@ -0,0 +1,283 @@
+## Global resource algebra management
+
+The type of Iris propositions `iProp Σ` is parameterized by a *global* list `Σ:
+gFunctors` of resource algebras that the proof may use.  (Actually this list
+contains functors instead of resource algebras, but you only need to worry about
+that when dealing with higher-order ghost state -- see "Camera functors" below.)
+
+In our proofs, we always keep the `Σ` universally quantified to enable composition of proofs.
+Each proof just assumes that some particular resource algebras are contained in that global list.
+This is expressed via the `inG Σ R` typeclass, which roughly says that `R ∈ Σ`.
+
+Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
+not have to expose to clients what exactly their resource algebras are. For
+example, in the [one-shot example](../tests/one_shot.v), we have:
+```coq
+Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+```
+The `:>` means that the projection `one_shot_inG` is automatically registered as
+an instance for type-class resolution.  If you need several resource algebras,
+just add more `inG` fields.  If you are using another module as part of yours,
+add a field like `one_shot_other :> otherG Σ`.
+
+Having defined the type class, we need to provide a way to instantiate it.  This
+is an important step, as not every resource algebra can actually be used: if
+your resource algebra refers to `Σ`, the definition becomes recursive.  That is
+actually legal under some conditions (see "Camera functors" below), but for now
+we will ignore that case.  We have to define a list that contains all the
+resource algebras we need:
+```coq
+Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
+```
+This time, there is no `Σ` in the context, so we cannot accidentally introduce a
+bad dependency.  If you are using another module as part of yours, add their
+`somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`.  (The
+`#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each
+other; together with a coercion from a single functor to a singleton list, this
+means lists can be nested arbitrarily.)
+
+Now we can define the one and only instance that our type class will ever need:
+```coq
+Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
+Proof. solve_inG. Qed.
+```
+The `subG` assumption here says that the list `one_shotΣ` is a sublist of the
+global list `Σ`.  Typically, this should be the only assumption your instance
+needs, showing that the assumptions of the module (and all the modules it
+uses internally) can trivially be satisfied by picking the right `Σ`.
+
+Now you can add `one_shotG` as an assumption to all your module definitions and
+proofs.  We typically use a section for this:
+```coq
+Section proof.
+Context `{!heapG Σ, !one_shotG Σ}.
+```
+Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
+which are assumptions that every HeapLang proof makes (they are related to
+defining the `↦` connective as well as the basic Iris infrastructure for
+invariants and WP).  For this purpose, `heapG` contains not only assumptions
+about `Σ`, it also contains some ghost names to refer to particular ghost state
+(see "global ghost state instances" below).
+
+The backtick (`` ` ``) is used to make anonymous assumptions and to automatically
+generalize the `Σ`.  When adding assumptions with backtick, you should most of
+the time also add a `!` in front of every assumption.  If you do not then Coq
+will also automatically generalize all indices of type-classes that you are
+assuming.  This can easily lead to making more assumptions than you are aware
+of, and often it leads to duplicate assumptions which breaks type class
+resolutions.
+
+## Resource algebra combinators
+
+Defining a new resource algebra `one_shotR` for each new proof and verifying all
+the algebra laws would be quite cumbersome, so instead Iris provides a rich set
+of resource algebra combinators that one can use to build up the desired
+resource algebras. For example, `one_shotR` is defined as follows:
+
+```coq
+Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
+```
+
+The suffixes `R` and `O` indicate that we are not working on the level of Coq
+types here, but on the level of `R`esource algebras and `O`FEs,
+respectively. Unfortunately this means we cannot use Coq's usual type notation
+(such as `*` for products and `()` for the unit type); we have to spell out the
+underlying OFE or resource algebra names instead.
+
+## Obtaining a closed proof
+
+To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
+`inG`, you have to assemble a list of functors of all the involved modules,
+and if your proof relies on some singleton (most do, at least indirectly; also
+see the next section), you have to call the respective initialization or
+adequacy lemma.  [For example](tests/one_shot.v):
+```coq
+Section client.
+  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+
+  Lemma client_safe : WP client {{ _, True }}%I.
+  (* ... *)
+End client.
+
+(** Assemble all functors needed by the [client_safe] proof. *)
+Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
+
+(** Apply [heap_adequacy] with this list of all functors. *)
+Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
+Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
+```
+
+## Advanced topic: Ghost state singletons
+
+Some Iris modules involve a form of "global state".  For example, defining the
+`↦` for HeapLang involves a piece of ghost state that matches the current
+physical heap.  The `gname` of that ghost state must be picked once when the
+proof starts, and then globally known everywhere.  Hence it is added to
+`gen_heapG`, the type class for the generalized heap module:
+```coq
+Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
+  gen_heap_name : gname
+}.
+```
+
+Such modules always need some kind of "initialization" to create an instance
+of their type class.  For example, the initialization for `heapG` is happening
+as part of [`heap_adequacy`](theories/heap_lang/adequacy.v); this in turn uses
+the initialization lemma for `gen_heapG` from
+[`gen_heap_init`](theories/base_logic/lib/gen_heap.v):
+```coq
+Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
+  (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
+```
+These lemmas themselves only make assumptions the way normal modules (those
+without global state) do, which are typically collected in a `somethingPreG`
+type class (such as `gen_heapPreG`):
+```coq
+Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V))
+}.
+```
+Just like in the normal case, `somethingPreG` type classes have an `Instance`
+showing that a `subG` is enough to instantiate them:
+```coq
+Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
+  subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
+Proof. solve_inG. Qed.
+```
+The initialization lemma then shows that the `somethingPreG` type class is
+enough to create an instance of the main `somethingG` class *below a view
+shift*.  This is written with an existential quantifier in the lemma because the
+statement after the view shift (`gen_heap_ctx σ` in this case) depends on having
+an instance of `gen_heapG` in the context.
+
+Given that these global ghost state instances are singletons, they must be
+assumed explicitly everywhere.  Bundling `heapG` in a module type class like
+`one_shotG` would lose track of the fact that there exists just one `heapG`
+instance that is shared by everyone.
+
+## Advanced topic: Camera functors and higher-order ghost state
+
+As we already alluded to, `Σ` actually consists of functors, not resource
+algebras. This enables you to use *higher-order ghost state*: ghost state that
+recursively refers to `iProp`.
+
+**Background: Iris Model.** To understand how this works, we have to dig a bit
+into the model of Iris. In Iris, the type of propositions `iProp` is described
+by the solution to the recursive domain equation:
+
+```coq
+iProp ≅ uPred (F (iProp))
+```
+
+Here, `uPred M` describes "propositions with resources of type `M`".  The
+peculiar aspect of this definition is that the notion of resources can itself
+refer to the set propositions that we are just defining; that dependency is
+expressed by `F`.  `F` is a user-chosen locally contractive bifunctor from COFEs
+to unital Cameras (a step-indexed generalization of unital resource
+algebras). Having just a single fixed `F` would however be rather inconvenient,
+so instead we have a list `Σ`, and then we define the global functor `F_global`
+roughly as follows:
+
+```coq
+F_global X := Π_{F ∈ Σ} gmap nat (F X)
+```
+
+In other words, each functor in `Σ` is applied to the recursive argument `X`,
+wrapped in a finite partial function, and then we take a big product of all of
+that.  The product ensures that all `F ∈ Σ` are available, and the `gmap` is
+needed to provide the proof rule `own_alloc`, which lets you create new
+instances of the given type of resource any time.
+
+However, this on its own would be too restrictive, as it requires all
+occurrences of `X` to be in positive positions (otherwise the functor laws
+would not hold for `F`).  To mitigate this, we instead work with "bifunctors":
+functors that take two arguments, `X` and `X⁻`, where `X⁻` is used for
+negative positions.  This leads us to the following domain equation:
+
+```coq
+iProp ≅ uPred (F_global (iProp,iProp))
+F_global (X,X⁻) := Π_{F ∈ Σ} gmap nat (F (X,X⁻))
+```
+
+To make this equation well-defined, the bifunctors `F ∈ Σ` need to be "contractive".
+For further details, see §7.4 of
+[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.3.pdf); here we
+describe the user-side Coq aspects of this approach.
+
+Below, when we say "functor", we implicitly mean "bifunctor".
+
+**Higher-order ghost state.** To use higher-order ghost state, you need to give
+a functor whose "hole" will later be filled with `iProp` itself. For example,
+let us say you would like to have ghost state of type `gmap K (agree (nat *
+later iProp))`, using the "type-level" `later` operator which ensures
+contractivity.  Then you will have to define a functor such as:
+
+```coq
+F (X,X⁻) := gmap K (agree (nat * ▶ X))
+```
+
+To make it convenient to construct such functors and prove their contractivity,
+we provide a number of abstractions:
+
+- [`cFunctor`](theories/algebra/ofe.v): functors from COFEs to OFEs.
+- [`rFunctor`](theories/algebra/cmra.v): functors from COFEs to cameras.
+- [`urFunctor`](theories/algebra/cmra.v): functors from COFEs to unital
+  cameras.
+
+Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
+`urFunctorContractive` which describe the subset of the above functors that are
+contractive.
+
+To compose these functors, we provide a number of combinators, e.g.:
+
+- `constOF (A : ofeT) : cFunctor           := λ (B,B⁻), A `
+- `idOF : cFunctor                         := λ (B,B⁻), B`
+- `prodOF (F1 F2 : cFunctor) : cFunctor    := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
+- `ofe_morOF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
+- `laterOF (F : cFunctor) : cFunctor       := λ (B,B⁻), later (F (B,B⁻))`
+- `agreeRF (F : cFunctor) : rFunctor       := λ (B,B⁻), agree (F (B,B⁻))`
+- `gmapURF K (F : rFunctor) : urFunctor    := λ (B,B⁻), gmap K (F (B,B⁻))`
+
+Note in particular how the functor for the function space, `ofe_morOF`, swaps
+`B` and `B⁻` for the functor `F1` describing the domain.  This reflects the fact
+that that functor is used in a negative position.
+
+Using these combinators, one can easily construct bigger functors in point-free
+style and automatically infer their contractivity, e.g:
+
+```coq
+F := gmaURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
+```
+
+which effectively defines the desired example functor
+`F := λ (B,B⁻), gmap K (agree (nat * later B))`.
+
+To make it a little bit more convenient to write down such functors, we make
+the constant functors (`constOF`, `constRF`, and `constURF`) a coercion, and
+provide the usual notation for products, etc. So the above functor can be
+written as follows:
+
+```coq
+F := gmapRF K (agreeRF (natO * ▶ ∙))
+```
+
+Basically, the functor can be written "as if" you were writing a resource
+algebra, except that there need to be extra "F" suffixes to indicate that we are
+working with functors, and the desired recursive `iProp` is replaced by the
+"hole" `∙`.
+
+Putting it all together, the `libG` typeclass and `libΣ` list of functors for
+your example would look as follows:
+
+```coq
+Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
+Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
+Proof. solve_inG. Qed.
+```
+
+It is instructive to remove the `â–¶` and see what happens: the `libG` class still
+works just fine, but `libΣ` complains that the functor is not contractive. This
+demonstrates the importance of always defining a `libΣ` alongside the `libG` and
+proving their relation.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 13b4e05aaef3fa9b9749cff8191b50fec1d2ca44..3de778074989ff8490913e049a2dee1ecb24d6b9 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl agree csum.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 40efb5efc3e972c6887bce976b8de1d1d4da568f..13230b72860e57a20aecb047bb4ed4f6c4f22069 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac agree csum.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index a01fafc469a8ce0a34a93f749c4b6b5366c451fa..96b2f643a536a9d8ce859d2697667a86bd451169 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics monpred.
 From iris.algebra Require Import frac.
+From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 091da0fedc4f885e741a91cbb37a6dc43b7e4c24..192810f68d89c15a840b0137cd8b597bdc053c63 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export bi.
 From iris.algebra Require Import frac.
+From iris.bi Require Export bi.
 From iris.base_logic Require Export bi.
 From iris Require Import options.
 Import bi.bi base_logic.bi.uPred.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index d02ce530697f2199d52f6c924a832f6468d87a84..2d99ad3c102b90743203fdd22c20cde5a704038d 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -1,6 +1,6 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index aa110f947f6232a3f671b6828513f65a7b54a7ec..cad3771656e9710fc039b90072bdc7ca3b2c2437 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import lib.excl_auth gmap agree.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index edc62ff7a345b709b882cee7c624347375c5bd01..0a4407c19ad0fd715cc27ec0c8ac25a26812396c 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Export frac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Export frac.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index ccd4ac39cf70d7b97817fe6de67f40db9fb42ac0..558fae055067fa77d4a9d79f4ebef5cd46022e49 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -1,6 +1,6 @@
 From stdpp Require Export coPset.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import wsat.
 From iris Require Import options.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index c30ba89986e7310b7294a2c46ca5b40aa70f2f76..523c5c22748811fd0158e93bcb4c567f24457b4c 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,7 +1,7 @@
 From stdpp Require Export namespaces.
+From iris.algebra Require Import gmap_view namespace_map agree frac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import gmap_view namespace_map agree frac.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index 096cdc0d66c948d2f46147feca61ba928c396e6c..c3592a927fbf79f3d7d916371734e81abbbe6042 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/theories/base_logic/lib/ghost_var.v
@@ -1,8 +1,8 @@
 (** A simple "ghost variable" of arbitrary type with fractional ownership.
 Can be mutated when fully owned. *)
+From iris.algebra Require Import frac_agree.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac_agree.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index adff4f6eb0a06733e346c854757bbc8bc6f9323a..5fa9cd8d0d8889f74b6a5abd58f7bd744d9935c4 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -1,6 +1,6 @@
 From stdpp Require Export namespaces.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.base_logic.lib Require Import wsat.
 From iris Require Import options.
diff --git a/theories/base_logic/lib/mnat.v b/theories/base_logic/lib/mnat.v
index 501fe90886b4974e3487db8c3bf14c3a77b990b1..b25f4358d47efa3f3f6bc2055cc1d26425cae1cf 100644
--- a/theories/base_logic/lib/mnat.v
+++ b/theories/base_logic/lib/mnat.v
@@ -8,9 +8,9 @@ lower-bound at [m] imply that [m ≤ n], and [mnat_update], which allows to
 increase the auth element. At any time the auth nat can be "snapshotted" with
 [mnat_get_lb] to produce a persistent lower-bound proposition. *)
 
-From iris.proofmode Require Import tactics.
 From iris.algebra.lib Require Import mnat_auth.
 From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index c900737bd28176cd1b2197febd06203f84e74f6f..9f3f659ce232615818ac3a201166f930cc44c4a9 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 586725300a542731901700695a9c5a1babccb4a3..f9915ee2b357ecfbed07c2b0b593e07408a23768 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import agree.
+From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export own.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 30ceaa1108423c9b6fec4c7edfb2a3c76707cd7a..329ead42a5efea3f83a025b1782129b8450f21b7 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Export sts.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 020d584ae096cb40cbbe06b09d2a8d8999c71fa1..c64dcebcdb96e2f3fcba1871562f5dad402eec01 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -1,6 +1,6 @@
 From stdpp Require Export coPset.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap_view gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 3db95759cafbaaa29c9e4d8ee8259fbdbaa35ad4..445ad37bad26078267ddd5c37ab0ca2e065a9068 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,6 +1,6 @@
 From stdpp Require Import finite.
-From iris.bi Require Import notation.
 From iris.algebra Require Export cmra updates.
+From iris.bi Require Import notation.
 From iris Require Import options.
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core.
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption] : core.
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 52ec4bebf2dd7d0fab0891695108aac0bb37336b..434592fd931fdb3b7f0fe39e0c920aedc6a6bb00 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -1,5 +1,4 @@
 From iris.bi Require Import interface derived_connectives updates.
-From iris.algebra Require Export ofe.
 From iris Require Import options.
 
 Notation "P |- Q" := (P ⊢ Q)
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index fdeb3a982771514003b786b90575c8b3ae70b39d..671a8ae13784a2815e9ecb3691b4d968da1e18db 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export interface.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export interface.
 From iris Require Import options.
 
 Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index d5fd0ae0c74431d58f633a86a492346946044a3a..aab10e497ef6f206e84b35a0bcd383c0750ae58a 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export derived_connectives.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export derived_connectives.
 From iris Require Import options.
 
 (* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index 1af9dd81e8fb0dbcf9edb8b867791d29cbb8f195..85b375a2c6ca203b317086b07e1611312f77401e 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export derived_laws.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export derived_laws.
 From iris Require Import options.
 
 Module bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 4a70ddb3b2027ca569efd5067e2141cf429f9a30..bb73cf16aff25a4fce9395006c53d5d532f4ee2e 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Import monoid.
 From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
-From iris.algebra Require Import monoid.
 From iris Require Import options.
 
 (* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index ba41b1898570fbaa64b031603b60e1da6a7271fb..dc7155fb2107c40fb631f7bf13524d146a542071 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export notation.
 From iris.algebra Require Export ofe.
+From iris.bi Require Export notation.
 From iris Require Import options.
 Set Primitive Projections.
 
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 7a8646f184447f1c6317d8e9b61e414442248f4f..c35d743797a539320a0d0e3390a20c1ee8786678 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,5 +1,5 @@
-From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.algebra Require Import monoid.
+From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 7ffc5a931c5d5409556ff25da5251dda12c436e7..1c66662702103c87e544257ff24143b9563d657b 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Import proofmode notation.
 From iris Require Import options.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 72109448c0034331d3cc1318bdcfb97da3164701..48537d024b8dd3b26a95d3055bcb2bcbc61d8308 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import lib.frac_auth numbers auth.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 9b10f92472869c843437e1be3b9f97258c6f5f32..0d033c5d1079ea5b8e266f27d3b965c54b916afc 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 1e5af4e7310de9c20b5c0c587799196ec5d57bd6..8f4986496c807a4cd75a824dd95079590a0f2079 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 850db347dbc634cdf2b8fce87b8bc69d1d2bb16b..5b202eaed32f998c5b48d80cf83e6d491486c7cc 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl auth gset.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index afb76b7dbb5aca8d66c8e01465ae8576759c5cbe..5e1ccb1e6eb14f5ec155fed82809002243ac3ead 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -2,8 +2,8 @@
 the Iris lifting lemmas. *)
 
 From stdpp Require Import fin_maps.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
+From iris.proofmode Require Import tactics.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 3a1bf860bb7c98029b957673fec65b44b9175b97..612af7f2996ec4101ee3209c06c81e4f18be33f0 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import wsat.
 From iris.program_logic Require Export weakestpre.
 From iris Require Import options.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 2a0fde9be9cfb4750221ddb65cf8fa66356e59e4..78e6ffcf9bdc044edb08677675c277bf42f4fc3f 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics classes.
 From iris.algebra Require Import lib.excl_auth.
+From iris.proofmode Require Import tactics classes.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 731f690798d8411b479846f275fea521d7dfd027..1825b3cd9779245e1de2c2f0e3c3c590c4b1998e 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.bi Require Import big_op fixpoint.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.program_logic Require Export total_weakestpre adequacy.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index b37062dc851953bc8efb739da6330397684c2df3..e77b6b44eff752ee9062629c38aed7470aa7e9ff 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Export base.
 From iris.bi Require Export bi.
 From iris.proofmode Require Import base.
-From iris.algebra Require Export base.
 From iris Require Import options.
 Import bi.