diff --git a/README.md b/README.md
index c517245a65adc0b775748b2b6ced05379ce35fd5..0ffe70b36eea827e34a3410f849cf5003d629645 100644
--- a/README.md
+++ b/README.md
@@ -111,22 +111,18 @@ mechanization in Coq:
 There are a number of small differences between the paper presentation
 of Actris and the formalization in Coq, that are briefly discussed here.
 
-- **Connectives for physical ownership of channels**
-
-    In the paper, physical ownership of a channel is formalized using a single
+- **Connectives for physical ownership of channels**  
+  In the paper, physical ownership of a channel is formalized using a single
   connective `(c1,c2) ↣ (vs1,vs2)`, while the mechanization has two connectives
   for the endpoints and one for connecting them, namely:
   - `chan_own γ Left vs1` and `chan_own γ Right vs1`
   - `is_chan N γ c1 c2`
-
-    Here, `γ` is a ghost name and `N` an invariant name. This setup is less
+  Here, `γ` is a ghost name and `N` an invariant name. This setup is less
   intuitive but gives rise to a more practical Jacobs/Piessens-style spec of
   `recv` that does not need a closing view shift (to handle the case that the
   buffer is empty).
-
-- **Later modalities in primitive rules for channels**
-
-    The primitive rules for `send` and `recv` (`send_spec` and `recv_spec` in
+- **Later modalities in primitive rules for channels**  
+  The primitive rules for `send` and `recv` (`send_spec` and `recv_spec` in
   [theories/channel/channel.v](theories/channel/channel.v)) contain three later
   (`â–·`) modalities, which are omitted for brevity's sake in the paper. These
   later modalities expose that these operations perform at least three steps in