diff --git a/algebra/upred.v b/algebra/upred.v
index 1005bf06fa78508d558d70aea253394f0d9d844a..369bc17622ccd60d81454e71560317fba74d66a1 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -957,7 +957,7 @@ Proof. intros P Q; apply later_mono. Qed.
 Global Instance later_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@uPred_later M).
 Proof. intros P Q; apply later_mono. Qed.
-Lemma later_True : (▷ True) ⊣⊢ True.
+Lemma later_True : ▷ True ⊣⊢ True.
 Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
 Lemma later_impl P Q : ▷ (P → Q) ⊢ (▷ P → ▷ Q).
 Proof.
@@ -969,7 +969,7 @@ Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
 Proof. apply: anti_symm; eauto using later_exist', later_exist_1. Qed.
 Lemma later_wand P Q : ▷ (P -★ Q) ⊢ (▷ P -★ ▷ Q).
 Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
-Lemma later_iff P Q : (▷ (P ↔ Q)) ⊢ (▷ P ↔ ▷ Q).
+Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ (▷ P ↔ ▷ Q).
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 Lemma löb_strong P Q : (P ∧ ▷ Q) ⊢ Q → P ⊢ Q.
 Proof.
@@ -1119,7 +1119,7 @@ Proof.
     cmra_timeless_included_l; eauto using cmra_validN_le.
 Qed.
 
-(* Always stable *)
+(* Persistence *)
 Global Instance const_persistent φ : PersistentP (■ φ : uPred M)%I.
 Proof. by rewrite /PersistentP always_const. Qed.
 Global Instance always_persistent P : PersistentP (â–¡ P).
@@ -1153,7 +1153,7 @@ Global Instance default_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
   PersistentP P → (∀ x, PersistentP (Ψ x)) → PersistentP (default P mx Ψ).
 Proof. destruct mx; apply _. Qed.
 
-(* Derived lemmas for always stable *)
+(* Derived lemmas for persistence *)
 Lemma always_always P `{!PersistentP P} : (□ P) ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
 Lemma always_intro P Q `{!PersistentP P} : P ⊢ Q → P ⊢ □ Q.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index fe35a51e6d93ee631b01471bdbac8abac5129aff..5171b8325a336513ea5c2b93143c4d1ecc4b76c3 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -28,17 +28,18 @@ Instance: Params (@uPred_big_sepS) 5.
 Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
   (at level 20, X at level 10, format "Π★{set  X }  Φ") : uPred_scope.
 
-(** * Always stability for lists *)
+(** * Persistence of lists of uPreds *)
 Class PersistentL {M} (Ps : list (uPred M)) :=
   persistentL : Forall PersistentP Ps.
 Arguments persistentL {_} _ {_}.
 
+(** * Properties *)
 Section big_op.
 Context {M : cmraT}.
 Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
 
-(* Big ops *)
+(** ** Big ops over lists *)
 Global Instance big_and_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_and M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M).
@@ -91,7 +92,7 @@ Proof. induction 1; simpl; auto with I. Qed.
 Lemma big_sep_elem_of Ps P : P ∈ Ps → Π★ Ps ⊢ P.
 Proof. induction 1; simpl; auto with I. Qed.
 
-(* Big ops over finite maps *)
+(** ** Big ops over finite maps *)
 Section gmap.
   Context `{Countable K} {A : Type}.
   Implicit Types m : gmap K A.
@@ -152,7 +153,7 @@ Section gmap.
   Qed.
 End gmap.
 
-(* Big ops over finite sets *)
+(** ** Big ops over finite sets *)
 Section gset.
   Context `{Countable A}.
   Implicit Types X : gset A.
@@ -213,7 +214,7 @@ Section gset.
   Qed.
 End gset.
 
-(* Always stable *)
+(** ** Persistence *)
 Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP (Π∧ Ps).
 Proof. induction 1; apply _. Qed.
 Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP (Π★ Ps).