diff --git a/tests/gset.ref b/tests/gset.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/gset.v b/tests/gset.v
new file mode 100644
index 0000000000000000000000000000000000000000..d8457668125172c1703ae606330fe5223a6581d4
--- /dev/null
+++ b/tests/gset.v
@@ -0,0 +1,15 @@
+From iris.algebra Require Import gset.
+
+Lemma test_op (X Y : gset nat) : X ⊆ Y → X ⋅ Y = Y.
+Proof. set_solver. Qed.
+Lemma test_included (X Y : gset nat) : X ≼ Y → X ∪ Y = Y ∧ X ∩ Y = X.
+Proof. set_solver. Qed.
+
+Lemma test_disj_included (X Y : gset nat) : GSet X ≼ GSet Y → X ∪ Y = Y ∧ X ∩ Y = X.
+Proof. set_solver. Qed.
+Lemma test_disj_equiv n : GSet (∅ : gset nat) ≡ GSet {[n]} → False.
+Proof. set_solver. Qed.
+Lemma test_disj_eq n : GSet (∅ : gset nat) = GSet {[n]} → False.
+Proof. set_solver. Qed.
+Lemma test_disj_valid (X Y : gset nat) : ✓ (GSet X ⋅ GSet Y) → X ∩ Y = ∅.
+Proof. set_solver. Qed.