diff --git a/iris/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
index da52b48cc41ad090b81ba08c6bb4b6ab363ff217..f947a7cb8e51582000df0d3c532e0c5628ce5ddb 100644
--- a/iris/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -59,9 +59,14 @@ Section excl_auth.
   Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
   Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
 
-  Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False.
+  Lemma excl_auth_auth_op_validN n a b : ✓{n} (●E a ⋅ ●E b) ↔ False.
+  Proof. apply auth_auth_op_validN. Qed.
+  Lemma excl_auth_auth_op_valid a b : ✓ (●E a ⋅ ●E b) ↔ False.
+  Proof. apply auth_auth_op_valid. Qed.
+
+  Lemma excl_auth_frag_op_validN n a b : ✓{n} (◯E a ⋅ ◯E b) ↔ False.
   Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
-  Lemma excl_auth_frag_valid_op_1_l a b : ✓ (◯E a ⋅ ◯E b) → False.
+  Lemma excl_auth_frag_op_valid a b : ✓ (◯E a ⋅ ◯E b) ↔ False.
   Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.
 
   Lemma excl_auth_update a b a' : ●E a ⋅ ◯E b ~~> ●E a' ⋅ ◯E a'.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index d467e21f5d564c77fc34db7291216b41c7f33b04..c7ec1a2dd42dc035cab04b6e9f67da0bdee5ed3d 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -100,7 +100,7 @@ Section lifting.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof.
-    rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_valid_op_1_l).
+    rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_op_valid).
   Qed.
   Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.