diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index c8c289e438114563a55f397183e9f5c58660891c..f8b24ad03ce1542d00f4b11e8bf1f25a0a0164fd 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -978,6 +978,17 @@ Lemma plainly_plainly P `{!Plain P} : ■ P ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); eauto. Qed.
 Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ ■ Q.
 Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
+Lemma plainly_alt P : ■ P ⊣⊢ P ≡ True.
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite -prop_ext. apply plainly_intro'. rewrite plainly_elim.
+    apply and_intro; apply impl_intro_r.
+    + apply True_intro.
+    + apply and_elim_l.
+  - rewrite internal_eq_sym (internal_eq_rewrite _ _ (λ P, ■ P)%I).
+    eapply impl_elim; first reflexivity.
+    rewrite plainly_pure. apply True_intro.
+Qed.
 
 Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
 Proof. by rewrite -{1}(plainly_plainly P) bupd_plainly. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 46768bd2e7ef7b26a0f3bd238585a00ed994747e..1e123fa4bb0058bce0980ab3320647fea1a7f2aa 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -650,7 +650,7 @@ Proof.
   - intros i a b; eapply Hf, ucmra_unit_validN.
 Qed.
 
-(* Functions *)
+(* Function extensionality *)
 Lemma ofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
 Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.