Make `Excl_included` and `Excl_includedN` bi-implications.

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.

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.