diff --git a/iris_core.v b/iris_core.v
index 5e873a88578b10bdfcd2b5d436d453d5fc132983..39a051e1c6149a9332071941cc5bf47156bd2816 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -201,9 +201,8 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
 
   Section Resources.
 
-    Lemma state_sep {σ g rf} (Hv : ↓(ex_own σ, g) · rf) : fst rf == 1 (ex_own σ)
-.
-    Proof. move: (ra_sep_prod Hv) => [Hs _]; exact: ra_sep_ex Hs. Qed.
+    Lemma state_sep {σ g rf} (Hv : ↓(ex_own σ, g) · rf) : fst rf == 1 (ex_own σ).
+    Proof. move: (ra_sep_prod Hv) => [Hs _]. by rewrite (ra_sep_ex Hs). Qed.
 
     Lemma state_fps {σ g σ' rf} (Hv : ↓(ex_own σ, g) · rf) : ↓(ex_own σ', g) · rf.
     Proof. exact: (ra_fps_fst (ra_fps_ex σ σ') rf). Qed.
diff --git a/lib/ModuRes/RAConstr.v b/lib/ModuRes/RAConstr.v
index b0c8cbefb511d8d223ec4134d60bdab11e9d4e62..43b6fd4a40eb6d86968fd704566bc31357530d6d 100644
--- a/lib/ModuRes/RAConstr.v
+++ b/lib/ModuRes/RAConstr.v
@@ -73,7 +73,7 @@ Section Exclusive.
     - intros [t1| |] [t2| |]; unfold ra_valid; simpl; now auto.
   Qed.
 
-  Lemma ra_sep_ex {t r} : ↓ex_own t · r -> r == 1 r.
+  Lemma ra_sep_ex {t r} : ↓ex_own t · r -> r = 1 r.
   Proof. by case: r. Qed.
 
   Lemma ra_fps_ex_any t {r} (Hr : ↓r) : ex_own t ⇝ r.