From fa7c7f01a39a0d835106d3ba677c388e69d6821c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Wed, 16 Mar 2022 10:07:38 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 theories/gmultiset.v | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index a4960ac2..730e3061 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -397,14 +397,9 @@ Section more_lemmas.
   Lemma list_to_set_disj_app l1 l2 :
     list_to_set_disj (l1 ++ l2) =@{gmultiset A} list_to_set_disj l1 ⊎ list_to_set_disj l2.
   Proof. induction l1; multiset_solver. Qed.
-  Lemma elem_of_list_to_set_disj x l:
+  Lemma elem_of_list_to_set_disj x l :
     x ∈@{gmultiset A} list_to_set_disj l ↔ x ∈ l.
-  Proof.
-    induction l as [|?? IH]; [set_solver|split].
-    - intros [->%gmultiset_elem_of_singleton| Hin]%gmultiset_elem_of_disj_union;
-        [set_solver|by right; apply IH].
-    - intros [-> |]%elem_of_cons; rewrite ?list_to_set_disj_cons; multiset_solver.
-  Qed.
+  Proof. induction l; set_solver. Qed.
   Global Instance list_to_set_disj_perm :
     Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)).
   Proof. induction 1; multiset_solver. Qed.
-- 
GitLab