From 3de1a0e8b0fb77993adb07d54d6e7da97347badd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jan 2021 16:43:40 +0100
Subject: [PATCH] add Cinl_valid, Cinr_valid

---
 iris/algebra/csum.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 8ff770410..95fe7172d 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -178,6 +178,11 @@ Proof. done. Qed.
 Lemma Cinr_op b b' : Cinr (b â‹… b') = Cinr b â‹… Cinr b'.
 Proof. done. Qed.
 
+Lemma Cinl_valid a : ✓ (Cinl a) ↔ ✓ a.
+Proof. done. Qed.
+Lemma Cinr_valid b : ✓ (Cinr b) ↔ ✓ b.
+Proof. done. Qed.
+
 Lemma csum_included x y :
   x ≼ y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼ a')
                       ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b').
-- 
GitLab