Doc changes from Ralf

docs/resource_algebras.md

@@ -20,13 +20,13 @@ Local Existing Instance one_shot_inG.
 Here, the projection `one_shot_inG` is 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 Σ`.
+`one_shot_other : otherG Σ`. All of these fields should be added to the `Local Existing Instances`.
 
-The code above enables these typeclass instances only in the surrounding file:
-where they are used to define the new abstraction by the library, while the
+The code above enables these typeclass instances only in the surrounding file
+where they are used to define the new abstractions by the library. The
 interface of these abstractions will only depend on the `one_shotG` class.
 Since `one_shot_inG` will be hidden from clients, they will not accidentally
-reuse it accidentally in their code.
+rely on it in their code.
 
 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