diff --git a/tests/sets.ref b/tests/sets.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/sets.v b/tests/sets.v
new file mode 100644
index 0000000000000000000000000000000000000000..9aea1a62b0bda62f4f1c373be747ed670ff9ba38
--- /dev/null
+++ b/tests/sets.v
@@ -0,0 +1,4 @@
+From stdpp Require Import sets.
+
+Lemma foo `{Set_ A C} (x : A) (X Y : C) : x ∈ X ∩ Y → x ∈ X.
+Proof. intros Hx. set_unfold in Hx. tauto. Qed.