diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 027517d48d8cf92a6de77a4c98540e729ee89d57..a61d5e214c3089430562acb09e1e5d0a3d05f852 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -118,10 +118,14 @@ Proof. by destruct mx. Qed.
 Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None.
 Proof. by destruct mx. Qed.
 
-Lemma Excl_includedN n a b  : Excl' a ≼{n} Excl' b → a ≡{n}≡ b.
-Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
-Lemma Excl_included a b : Excl' a ≼ Excl' b → a ≡ b.
-Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
+Lemma Excl_includedN n a b  : Excl' a ≼{n} Excl' b ↔ a ≡{n}≡ b.
+Proof.
+  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
+Qed.
+Lemma Excl_included a b : Excl' a ≼ Excl' b ↔ a ≡ b.
+Proof.
+  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
+Qed.
 End excl.
 
 Arguments exclO : clear implicits.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 72e75d5cdbd22df474cfac8a1bb729f26bb7595f..7098222ab80bd4aadcb74aa782204dd154a9ef9f 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -90,8 +90,8 @@ Section lifting.
   Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
-    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_both_valid.
-    by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
+    by iDestruct (own_valid_2 with "Hσ● Hσ◯")
+      as %[->%Excl_included _]%auth_both_valid.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.