diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index fd36a646ab8196675fee69e8543c1f1cbf9cf921..9e645124601af095c1088a20632a75bfdc66826f 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -208,7 +208,7 @@ Proof.
   apply impl_intro_l. rewrite left_absorb. auto.
 Qed.
 
-Lemma exists_impl_forall {A} P (Ψ : A → PROP) :
+Lemma exist_impl_forall {A} P (Ψ : A → PROP) :
   ((∃ x : A, Ψ x) → P) ⊣⊢ ∀ x : A, Ψ x → P.
 Proof.
   apply equiv_spec; split.