diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 304ac0cb64360569344a3884ed6a2ec861a6891b..99e1fbadefd93599f6c8f1d3a7701094ddd5ce30 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -250,8 +250,8 @@ Section restate.
   Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
   Proof. apply later_soundness. Qed.
 
-  (** All of these sealing lemmas are partially applied so that they also rewrite
-  under binders. *)
+  (** We restate the unsealing lemmas for the BI layer. The sealing lemmas
+  are partially applied so that they also rewrite under binders. *)
   Local Lemma uPred_emp_unseal : bi_emp = @upred.uPred_pure_def M True.
   Proof. by rewrite -upred.uPred_pure_unseal. Qed.
   Local Lemma uPred_pure_unseal : bi_pure = @upred.uPred_pure_def M.
@@ -291,8 +291,7 @@ Section restate.
     upred.uPred_ownM_unseal, upred.uPred_cmra_valid_unseal, @uPred_bupd_unseal).
 End restate.
 
-(** New unseal tactic that also unfolds the BI layer.
-  This is used by [base_logic.algebra] and [base_logic.bupd_alt]. *)
-
+(** The final unseal tactic that also unfolds the BI layer. This is used by
+[base_logic.algebra] and [base_logic.bupd_alt]. *)
 Ltac unseal := rewrite !uPred_unseal /=.
 End uPred.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 53b933508d9be11b4e31d46e6ec78921960fd299..06bd825af2a46e7afd82f8e8b8c6e58fe9f4381f 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -294,7 +294,8 @@ Section monPred_defs.
 End monPred_defs.
 
 (** This is not the final collection of unsealing lemmas, below we redefine
-[monPred_unseal] to use the projections of the BI canonical structures. *)
+[monPred_unseal] to also unfold the BI layer (i.e., the projections of the BI
+structures/classes). *)
 Local Definition monPred_unseal :=
   (@monPred_embed_unseal, @monPred_emp_unseal, @monPred_pure_unseal,
    @monPred_objectively_unseal, @monPred_subjectively_unseal,
@@ -388,7 +389,8 @@ Section instances.
     {| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
        bi_bi_later_mixin := monPred_bi_later_mixin |}.
 
-  (** Restate the unseal lemmas, but now with the projections of [bi]. *)
+  (** We restate the unsealing lemmas so that they also unfold the BI layer. The
+  sealing lemmas are partially applied so that they also work under binders. *)
   Local Lemma monPred_emp_unseal :
     bi_emp = @monPred_defs.monPred_emp_def I PROP.
   Proof. by rewrite -monPred_defs.monPred_emp_unseal. Qed.
@@ -423,9 +425,10 @@ Section instances.
     bi_later = @monPred_defs.monPred_later_def I PROP.
   Proof. by rewrite -monPred_defs.monPred_later_unseal. Qed.
 
-  (** This definition only includes the unseal lemmas for the bi connectives.
+  (** This definition only includes the unseal lemmas for the [bi] connectives.
   After we have defined the right class instances, we define [monPred_unseal],
-  which also includes embed/internal_eq/bupd/fupd/plainly. *)
+  which also includes [embed], [internal_eq], [bupd], [fupd], [plainly],
+  [monPred_objectively], [monPred_subjectively] and [monPred_in]. *)
   Local Definition monPred_unseal_bi :=
     (monPred_emp_unseal, monPred_pure_unseal, monPred_and_unseal,
     monPred_or_unseal, monPred_impl_unseal, monPred_forall_unseal,
@@ -540,7 +543,7 @@ Section instances.
   Proof. by rewrite -monPred_defs.monPred_plainly_unseal. Qed.
 
   (** And finally the proper [unseal] tactic (which we also redefine outside
-  of the section). *)
+  of the section since Ltac definitions do not outlive a section). *)
   Local Definition monPred_unseal :=
     (monPred_unseal_bi, @monPred_embed_unseal, @monPred_internal_eq_unseal,
     @monPred_bupd_unseal, @monPred_fupd_unseal, @monPred_plainly_unseal,
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index 6d46d6f65a27b77f9d761137f9426aaeb5ad5d4e..a7839f6af9b31af557e7068a439cb8b38e65ed8e 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -186,8 +186,8 @@ Section restate.
   Lemma later_soundness (P : siProp) : (⊢ ▷ P) → ⊢ P.
   Proof. apply later_soundness. Qed.
 
-  (** All of these sealing lemmas are partially applied so that they also rewrite
-  under binders. *)
+  (** We restate the unsealing lemmas so that they also unfold the BI layer. The
+  sealing lemmas are partially applied so that they also work under binders. *)
   Local Lemma siProp_emp_unseal : bi_emp = @siprop.siProp_pure_def True.
   Proof. by rewrite -siprop.siProp_pure_unseal. Qed.
   Local Lemma siProp_pure_unseal : bi_pure = @siprop.siProp_pure_def.
@@ -223,5 +223,6 @@ Section restate.
     siProp_plainly_unseal, siProp_persistently_unseal, siProp_later_unseal).
 End restate.
 
+(** The final unseal tactic that also unfolds the BI layer. *)
 Ltac unseal := rewrite !siProp_unseal /=.
 End siProp.