From dd04c27a5d89447b2fa976e42dbcfb5bdb501f7b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Mar 2021 14:01:23 +0100
Subject: [PATCH] Shorten proof of `singleton_union_difference`.

---
 theories/sets.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/theories/sets.v b/theories/sets.v
index 8e95e8d4..6e5d84be 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -795,10 +795,7 @@ Section set.
     Proof. set_solver. Qed.
     Lemma singleton_union_difference X Y x :
       {[x]} ∪ (X ∖ Y) ≡ ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
-    Proof.
-      intro y; split; intros Hy; [ set_solver | ].
-      destruct (decide (y ∈ ({[x]} : C))); set_solver.
-    Qed.
+    Proof. intro y; destruct (decide (y ∈@{C} {[x]})); set_solver. Qed.
 
     Context `{!LeibnizEquiv C}.
     Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
-- 
GitLab