diff --git a/modularity/MiniMutableSet.scala b/modularity/MiniMutableSet.scala
new file mode 100644
index 00000000..2fc8259d
--- /dev/null
+++ b/modularity/MiniMutableSet.scala
@@ -0,0 +1,14 @@
+package modularity
+
+import stainless.collection.List
+import stainless.annotation.mutable
+
+object MiniMutableSet:
+
+  @mutable
+  final case class MiniMutSet[V](private var content: List[V]) extends MiniMutableSetInterface.iMiniMutableSet[V]:
+    override def contains(v: V): Boolean = content.contains(v)
+    override def add(v: V): Unit = {
+      content = v :: content
+    }.ensuring(_ => true)
+end MiniMutableSet
diff --git a/modularity/MiniMutableSetInterface.scala b/modularity/MiniMutableSetInterface.scala
new file mode 100644
index 00000000..99733c0b
--- /dev/null
+++ b/modularity/MiniMutableSetInterface.scala
@@ -0,0 +1,33 @@
+package modularity
+
+
+import stainless.annotation.mutable
+import stainless.annotation.pure
+import stainless.annotation.law
+
+
+
+object MiniMutableSetInterface:
+  @mutable
+  trait iMiniMutableSet[V]:
+    @pure def contains(v: V): Boolean
+    def add(v: V): Unit = {
+      ??? : Unit
+    }.ensuring(_ => contains(v))
+
+    // @law @pure @ghost def addContains(v: V): Boolean = {
+    //   val snap = snapshot(this)
+    //   snap.add(v)
+    //   snap.contains(v)
+    // }
+  end iMiniMutableSet
+end MiniMutableSetInterface
+
+
+object MiniSetUsage:
+  import MiniMutableSetInterface._
+  def testMiniMutableSet(s: iMiniMutableSet[BigInt]): Unit = {
+    s.add(1)
+    assert(s.contains(1))
+  }
+end MiniSetUsage
diff --git a/modularity/iMutableSet.scala b/modularity/MutableSetInterface.scala
similarity index 100%
rename from modularity/iMutableSet.scala
rename to modularity/MutableSetInterface.scala