diff --git a/liquid-containers.cabal b/liquid-containers.cabal
--- a/liquid-containers.cabal
+++ b/liquid-containers.cabal
@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-containers
-version:            0.6.2.1
+version:            0.6.4.1
 synopsis:           LiquidHaskell specs for the containers package
 description:        LiquidHaskell specs for the containers package.
 license:            BSD3
@@ -15,7 +15,7 @@
 data-files:           src/Data/Set.spec
 
 custom-setup
-  setup-depends: Cabal, base, liquidhaskell
+  setup-depends: Cabal<4, base<5, liquidhaskell
 
 library
   exposed-modules:    Data.Containers.ListUtils
@@ -49,9 +49,10 @@
                       Utils.Containers.Internal.StrictPair
   hs-source-dirs:     src
   build-depends:      liquid-base          < 5
-                    , containers           >= 0.6.2.1 && < 0.7
-                    , liquidhaskell        >= 0.8.10.1
+                    , containers           >= 0.6.4.1 && < 0.7
+                    , liquidhaskell        >= 0.9.0.2
   default-language:   Haskell2010
   default-extensions: PackageImports
   if impl(ghc >= 8.10)
     ghc-options: -fplugin=LiquidHaskell
+  
diff --git a/src/Data/Set.spec b/src/Data/Set.spec
--- a/src/Data/Set.spec
+++ b/src/Data/Set.spec
@@ -2,38 +2,38 @@
 
 embed Data.Set.Internal.Set as Set_Set
 
-// ----------------------------------------------------------------------------------------------
-// -- | Logical Set Operators: Interpreted "natively" by the SMT solver -------------------------
-// ----------------------------------------------------------------------------------------------
+//  ----------------------------------------------------------------------------------------------
+//  -- | Logical Set Operators: Interpreted "natively" by the SMT solver -------------------------
+//  ----------------------------------------------------------------------------------------------
 
 
-// union
+//  union
 measure Set_cup  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
 
-// intersection
+//  intersection
 measure Set_cap  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
 
-// difference
+//  difference
 measure Set_dif   :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
 
-// singleton
+//  singleton
 measure Set_sng   :: a -> (Data.Set.Internal.Set a)
 
-// emptiness test
+//  emptiness test
 measure Set_emp   :: (Data.Set.Internal.Set a) -> GHC.Types.Bool
 
-// empty set
+//  empty set
 measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Internal.Set a)
 
-// membership test
+//  membership test
 measure Set_mem  :: a -> (Data.Set.Internal.Set a) -> GHC.Types.Bool
 
-// inclusion test
+//  inclusion test
 measure Set_sub  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> GHC.Types.Bool
 
-// ---------------------------------------------------------------------------------------------
-// -- | Refined Types for Data.Set Operations --------------------------------------------------
-// ---------------------------------------------------------------------------------------------
+//  ---------------------------------------------------------------------------------------------
+//  -- | Refined Types for Data.Set Operations --------------------------------------------------
+//  ---------------------------------------------------------------------------------------------
 
 isSubsetOf    :: (GHC.Classes.Ord a) => x:(Data.Set.Internal.Set a) -> y:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_sub x y}
 member        :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_mem x xs}
@@ -49,11 +49,14 @@
 difference    :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_dif xs ys}
 
 fromList :: GHC.Classes.Ord a => xs:[a] -> {v:Data.Set.Internal.Set a | v = listElts xs}
+toList   :: GHC.Classes.Ord a => s:Data.Set.Internal.Set a -> {xs:[a] | s = listElts xs}
 
-// ---------------------------------------------------------------------------------------------
-// -- | The set of elements in a list ----------------------------------------------------------
-// ---------------------------------------------------------------------------------------------
+//  ---------------------------------------------------------------------------------------------
+//  -- | The set of elements in a list ----------------------------------------------------------
+//  ---------------------------------------------------------------------------------------------
 
 measure listElts :: [a] -> (Data.Set.Internal.Set a)
-listElts([])   = {v | (Set_emp v)}
-listElts(x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }
+  listElts []     = {v | (Set_emp v)}
+  listElts (x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }
+
+