From 736b17dca694d4cbb8c6f687be78489346007b9b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Jul 2019 12:11:13 +0200
Subject: [PATCH] Weaken premise of `gmultiset_local_update_dealloc`.

---
 theories/algebra/gmultiset.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 576918daa..bd4637134 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -73,9 +73,10 @@ Section gmultiset.
   Proof. apply gmultiset_local_update. by rewrite (comm_L _ Y) assoc_L. Qed.
 
   Lemma gmultiset_local_update_dealloc X Y X' :
-    X' ⊆ X → X' ⊆ Y → (X,Y) ~l~> (X ∖ X', Y ∖ X').
+    X' ⊆ Y → (X,Y) ~l~> (X ∖ X', Y ∖ X').
   Proof.
-    intros ->%gmultiset_disj_union_difference ->%gmultiset_disj_union_difference.
+    intros ->%gmultiset_disj_union_difference. apply local_update_total_valid.
+    intros _ _ ->%gmultiset_included%gmultiset_disj_union_difference.
     apply gmultiset_local_update. apply gmultiset_eq=> x.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
     lia.
-- 
GitLab