From 4f0acc79f2e54da185600bd0f8f6db60fd6f37b2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Sep 2016 23:18:57 +0200
Subject: [PATCH] Lemma for inclusion of excl similar to dec_agree.

---
 algebra/excl.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/algebra/excl.v b/algebra/excl.v
index f93c4339a..bd1bc8612 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -120,11 +120,11 @@ Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None.
 Proof. by destruct mx. Qed.
 Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None.
 Proof. by destruct mx. Qed.
-Lemma Excl_includedN n a mx : ✓{n} mx → Excl' a ≼{n} mx ↔ mx ≡{n}≡ Excl' a.
-Proof.
-  intros Hvalid; split; [|by intros ->].
-  intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
-Qed.
+
+Lemma Excl_includedN n a b  : Excl' a ≼{n} Excl' b → a ≡{n}≡ b.
+Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
+Lemma Excl_included a b : Excl' a ≼ Excl' b → a ≡ b.
+Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
 End excl.
 
 Arguments exclC : clear implicits.
-- 
GitLab