From c0e3323a14ea71831f9def6402d812a4f0bbffdf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Aug 2023 09:28:21 +0200
Subject: [PATCH] add pair_dist

---
 iris/algebra/ofe.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 64e454a5c..82d6cf079 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -860,6 +860,10 @@ Section product.
   Global Instance prod_ofe_discrete :
     OfeDiscrete A → OfeDiscrete B → OfeDiscrete prodO.
   Proof. intros ?? [??]; apply _. Qed.
+
+  Lemma pair_dist n (a1 a2 : A) (b1 b2 : B) :
+    (a1, b1) ≡{n}≡ (a2, b2) ↔ a1 ≡{n}≡ a2 ∧ b1 ≡{n}≡ b2.
+  Proof. reflexivity. Qed.
 End product.
 
 Global Arguments prodO : clear implicits.
-- 
GitLab