diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index ec6c8d78aa1f38ffbca1a9cd90531d4ba0c22b7a..c0aa5b1ffbaa92f8f7f52b005488cc298825741c 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -673,6 +673,15 @@ Proof. apply (anti_symm _); auto using True_sep_2. Qed.
 Lemma sep_True P `{!Absorbing P} : P ∗ True ⊣⊢ P.
 Proof. by rewrite comm True_sep. Qed.
 
+Lemma True_emp_iff_BiAffine :
+  BiAffine PROP ↔ (True ⊢ emp).
+Proof.
+  split.
+  - intros ?. exact: affine.
+  - rewrite /BiAffine /Affine=>Hemp ?. rewrite -Hemp.
+    exact: True_intro.
+Qed.
+
 Section bi_affine.
   Context `{BiAffine PROP}.