From 8a295caf8d31d23f629ecc7357de3a21165109a3 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Wed, 31 Jan 2024 02:17:21 +0100
Subject: [PATCH] Proved admitted ghost lemma

---
 theories/channel/multi_proto.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/channel/multi_proto.v b/theories/channel/multi_proto.v
index 898b391..8cab819 100644
--- a/theories/channel/multi_proto.v
+++ b/theories/channel/multi_proto.v
@@ -1140,7 +1140,12 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
     own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p1))) -∗
     own γ (gmap_view_frag j (DfracOwn 1) (Excl' (Next p2))) -∗
     ⌜i ≠ j⌝.
-  Proof. Admitted.
+  Proof.
+    iIntros "Hown Hown'" (->).
+    iDestruct (own_valid_2 with "Hown Hown'") as "H".
+    rewrite uPred.cmra_valid_elim.
+    iDestruct "H" as %H%gmap_view_frag_op_validN. by destruct H.
+  Qed.
 
   Lemma iProto_step γ i j m1 m2 p1 v :
     iProto_ctx γ -∗
-- 
GitLab