From 307fdbdd511da78ead16338378b06b2d589a44de Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Sep 2016 22:31:46 +0200
Subject: [PATCH] Prove lemma cmra_valid_included.

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

diff --git a/algebra/cmra.v b/algebra/cmra.v
index c0c4dc515..f9c689fad 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -342,6 +342,8 @@ Global Instance cmra_included_trans: Transitive (@included A _ _).
 Proof.
   intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2). by rewrite assoc -Hy -Hz.
 Qed.
+Lemma cmra_valid_included x y : ✓ y → x ≼ y → ✓ x.
+Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_valid_op_l. Qed.
 Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x.
 Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
 Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x.
-- 
GitLab