diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index a7c13e15fb9d5c0a44e870107827cfd53e7884be..2850a5921863988d47bda4ee52238d4335c8606f 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -584,7 +584,7 @@ Proof. unseal. by destruct mx. Qed.
 (* Functions *)
 Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
-Lemma cofe_moreC_equivI {A B : cofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma cofe_morC_equivI {A B : cofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
 End primitive.
 End uPred_primitive.