From a18865f79847f980471258e4d9dc22cf682dae4b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 3 Jul 2019 14:26:36 +0200
Subject: [PATCH] =?UTF-8?q?Add=20lemmas=20for=20`=E2=89=BC`=20of=20`Cinl`?=
 =?UTF-8?q?=20and=20`Cinr`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/algebra/csum.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index d3ff72dcf..a16994265 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -189,6 +189,10 @@ Proof.
     + exists (Cinl c); by constructor.
     + exists (Cinr c); by constructor.
 Qed.
+Lemma Cinl_included a a' : Cinl a ≼ Cinl a' ↔ a ≼ a'.
+Proof. rewrite csum_included. naive_solver. Qed.
+Lemma Cinr_included b b' : Cinr b ≼ Cinr b' ↔ b ≼ b'.
+Proof. rewrite csum_included. naive_solver. Qed.
 
 Lemma csum_includedN n x y :
   x ≼{n} y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a')
-- 
GitLab