diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 13bfe0465e9261b32ae69613f4192af7482a2414..480b66ebec090aead0ba6807c3ba04923f79388d 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -113,7 +113,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'C
                         ) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
@@ -127,7 +127,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :
                        λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
-   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO)
@@ -142,7 +142,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :
                                 (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
-   format "'[   ' 'AU'  '<<'  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
@@ -151,10 +151,10 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200,
-   format "'[   ' 'AU'  '<<'  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 (** Notation: Atomic accessors *)
-Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
               (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
               Eo Ei
@@ -173,9 +173,9 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 ..
                      ) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
               (TB:=TeleO)
               Eo Ei
@@ -188,9 +188,9 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM
                         λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
               (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
               Eo Ei
@@ -204,9 +204,9 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM
                         (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
               (TB:=TeleO)
               Eo Ei
@@ -216,7 +216,7 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200,
-   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 (** Lemmas about AU *)
 Section lemmas.
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 006be9ca791de026c91cdd643dfa5e74bfe9a0ab..4d1b42215c852277fc9c155d4d6116a36ba0c4e9 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -42,7 +42,7 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v
                         ) .. )
   )
   (at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv' '[     ' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  ']' '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+   format "'[hv' '<<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
   : bi_scope.
 
 Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
@@ -62,7 +62,7 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
                         ) .. )
   )
   (at level 20, E, α, β, v at level 200, x1 binder, xn binder,
-   format "'[hv' '[     ' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  ']' '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+   format "'[hv' '<<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
   : bi_scope.
 
 Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
@@ -79,7 +79,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
                          (λ y1, .. (λ yn, v%V) .. ))
   )
   (at level 20, E, α, β, v at level 200, y1 binder, yn binder,
-   format "'[hv' '[     ' '<<<'  α  '>>>'  ']' '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
   : bi_scope.
 
 Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
@@ -92,7 +92,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
              (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
   )
   (at level 20, E, α, β, v at level 200,
-   format "'[hv' '[     ' '<<<'  α  '>>>'  ']' '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
   : bi_scope.
 
 (** Theory *)
diff --git a/tests/atomic.ref b/tests/atomic.ref
index fba1915ac32043440bf4d43621ab2b7f00227015..532b1a1366e993cbcc9fdb19a513d70b0439f853 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -9,8 +9,9 @@
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
-  AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0 ABORT l ↦ v >> 
-       @ ⊤ ∖ ∅, ∅ << l ↦{q} v0, COMM Q -∗ Q >>
+  AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
+       @ ⊤ ∖ ∅, ∅ 
+       << l ↦{q} v0, COMM Q -∗ Q >>
   
 "non_laterable"
      : string
@@ -24,8 +25,9 @@
   ============================
   "HP" : â–· P
   --------------------------------------∗
-  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> 
-       @ ⊤ ∖ ∅, ∅ << l ↦{q} v, COMM True >>
+  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
+       @ ⊤ ∖ ∅, ∅ 
+       << l ↦{q} v, COMM True >>
   
 1 goal
   
@@ -37,8 +39,9 @@
   ============================
   "HP" : â–· P
   --------------------------------------∗
-  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> 
-       @ ⊤ ∖ ∅, ∅ << l ↦{q} v, COMM True >>
+  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
+       @ ⊤ ∖ ∅, ∅ 
+       << l ↦{q} v, COMM True >>
   
 "printing"
      : string
@@ -67,10 +70,12 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << ∀ x : val, P x
-              ABORT AU << ∀ x : val, P x >> @ ⊤ ∖ ∅, ∅ 
-                       << ∃ y : val, P y, COMM Φ #() >> >> 
-           @ ⊤ ∖ ∅, ∅ << ∃ y : val, P y, COMM Φ #() >>
+  _ : AACC << ∀ x : val, P x,
+              ABORT AU << ∀ x : val, P x >>
+                       @ ⊤ ∖ ∅, ∅ 
+                       << ∃ y : val, P y, COMM Φ #() >> >>
+           @ ⊤ ∖ ∅, ∅ 
+           << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -99,10 +104,12 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << ∀ x : val, l ↦ x
-              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ 
-                       << l ↦ x, COMM Φ #() >> >> 
-           @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
+  _ : AACC << ∀ x : val, l ↦ x,
+              ABORT AU << ∀ x : val, l ↦ x >>
+                       @ ⊤ ∖ ∅, ∅ 
+                       << l ↦ x, COMM Φ #() >> >>
+           @ ⊤ ∖ ∅, ∅ 
+           << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -131,10 +138,12 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ 
-                       << ∃ y : val, l ↦ y, COMM Φ #() >> >> 
-           @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+  _ : AACC << l ↦ #(),
+              ABORT AU << l ↦ #() >>
+                       @ ⊤ ∖ ∅, ∅ 
+                       << ∃ y : val, l ↦ y, COMM Φ #() >> >>
+           @ ⊤ ∖ ∅, ∅ 
+           << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -163,9 +172,10 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >> 
-           @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
+  _ : AACC << l ↦ #(),
+              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >>
+           @ ⊤ ∖ ∅, ∅ 
+           << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -177,7 +187,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> 
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
       code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
@@ -187,7 +197,8 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤ ∖ ∅, ∅ 
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >>
+            @ ⊤ ∖ ∅, ∅ 
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -198,7 +209,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> 
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
@@ -209,7 +220,8 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+            @ ⊤ ∖ ∅, ∅ 
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -219,7 +231,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> 
+  ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
       code @ ∅
     <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
@@ -230,7 +242,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> 
+  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
          @ ⊤ ∖ ∅, ∅ 
          << ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
             l ↦ xx, COMM Φ #() >>
@@ -243,7 +255,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> 
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
     <<< l ↦ x, RET #() >>>
 1 goal
@@ -253,8 +265,9 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
-            @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤ ∖ ∅, ∅ 
+            << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -265,7 +278,7 @@
   l : loc
   x : val
   ============================
-  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> 
+  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
@@ -276,8 +289,9 @@
   x : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
-            @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤ ∖ ∅, ∅ 
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -288,7 +302,7 @@
   l : loc
   x : val
   ============================
-  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> 
+  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
     <<< l ↦ #(), RET #() >>>
 1 goal
@@ -299,8 +313,9 @@
   x : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
-            @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤ ∖ ∅, ∅ 
+            << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -311,7 +326,7 @@
   l : loc
   xx, yyyy : val
   ============================
-  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> 
+  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
       code @ ∅
     <<< l ↦ yyyy, RET #() >>>
 1 goal
@@ -322,8 +337,9 @@
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
-            l ↦ xx >> @ ⊤ ∖ ∅, ∅ << l ↦ yyyy, COMM Φ #() >>
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+            @ ⊤ ∖ ∅, ∅ 
+            << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -334,7 +350,7 @@
   l : loc
   xx, yyyy : val
   ============================
-  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> 
+  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
       code @ ∅
     <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
@@ -346,7 +362,8 @@
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤ ∖ ∅, ∅ 
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+            @ ⊤ ∖ ∅, ∅ 
             << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
                l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
@@ -363,7 +380,8 @@
   ============================
   "AU" : ∃ x : val, P x ∗
            (P x ={∅,⊤}=∗
-            AU << ∀ x0 : val, P x0 >> @ ⊤ ∖ ∅, ∅ 
+            AU << ∀ x0 : val, P x0 >>
+               @ ⊤ ∖ ∅, ∅ 
                << ∃ y : val, P y, COMM Φ #() >>)
            ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗