diff --git a/theories/sets.v b/theories/sets.v
index 8e95e8d45f9acdef9a8c80c2f8d81691f29da107..6e5d84be44a85471bff399b6e2c3bf5e4fded0f4 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.