From a82dbaf9c3c94e18c3592d5281d431b8bd37e44c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 24 May 2019 17:45:10 +0200
Subject: [PATCH] pair_valid

---
 theories/algebra/cmra.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 9df5355cd..7059e8b61 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1116,6 +1116,8 @@ Section prod.
 
   Lemma pair_op (a a' : A) (b b' : B) : (a, b) â‹… (a', b') = (a â‹… a', b â‹… b').
   Proof. done. Qed.
+  Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
+  Proof. done. Qed.
 
   Global Instance prod_cmra_total : CmraTotal A → CmraTotal B → CmraTotal prodR.
   Proof.
-- 
GitLab