diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 9b194ac4fe14046b05f11f1633d15693a7ea16ce..1f402b14e525bee08c6b98ee50ad4740a72ce031 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -306,7 +306,9 @@ Lemma insert_op m1 m2 i x y :
 Proof. by rewrite (insert_merge (â‹…) m1 m2 i (x â‹… y) x y). Qed.
 
 Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
-  x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
+  x ~~>: P →
+  (∀ y, P y → Q (<[i:=y]>m)) →
+  <[i:=x]>m ~~>: Q.
 Proof.
   intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm.
   destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index b4d5e520d84eacf0575e11b0c0b1c6f86a470050..83d923854e9323e1730bbb88053c4401d12e18e4 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -134,7 +134,8 @@ Section gset_disj.
 
   Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
     (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
-    (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
+    (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) →
+    GSet X ~~>: Q.
   Proof.
     intros Hfresh HQ.
     apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].