diff --git a/StandardLibrary/src/Sets.dfy b/StandardLibrary/src/Sets.dfy
index 2a6be71bd..b20bc07ef 100644
--- a/StandardLibrary/src/Sets.dfy
+++ b/StandardLibrary/src/Sets.dfy
@@ -8,11 +8,11 @@ module {:extern "SortedSets"} SortedSets {
   import opened StandardLibrary
   import Seq
 
-  method {:extern "SetToOrderedSequence"} ComputeSetToOrderedSequence<T(==)>(s: set<seq<T>>, less: (T, T) -> bool) returns (res: seq<seq<T>>)
+  method {:extern "SetToOrderedSequence"} ComputeSetToOrderedSequence<T(==, !new)>(s: set<seq<T>>, less: (T, T) -> bool) returns (res: seq<seq<T>>)
     requires Trichotomous(less) && Transitive(less)
     ensures res == SetToOrderedSequence(s, less)
 
-  function method {:extern "SetToOrderedSequence2"} ComputeSetToOrderedSequence2<T(==)>(
+  function method {:extern "SetToOrderedSequence2"} ComputeSetToOrderedSequence2<T(==, !new)>(
     s: set<seq<T>>,
     less: (T, T) -> bool
   )
@@ -25,7 +25,7 @@ module {:extern "SortedSets"} SortedSets {
     ensures forall k <- s :: k in res
     ensures |res| == |s|
 
-  function method {:extern "SetToSequence"} ComputeSetToSequence<T(==)>(
+  function method {:extern "SetToSequence"} ComputeSetToSequence<T(==, !new)>(
     s: set<T>
   )
     : (res: seq<T>)
diff --git a/StandardLibrary/src/Sorting.dfy b/StandardLibrary/src/Sorting.dfy
index d3d4957ad..f5ad91745 100644
--- a/StandardLibrary/src/Sorting.dfy
+++ b/StandardLibrary/src/Sorting.dfy
@@ -122,7 +122,7 @@ module Sorting {
    * Sorting routines
    */
 
-  method {:vcs_split_on_every_assert} SelectionSort<Data>(a: array<Data>, below: (Data, Data) -> bool)
+  method {:vcs_split_on_every_assert} SelectionSort<Data(!new)>(a: array<Data>, below: (Data, Data) -> bool)
     requires StandardLibrary.Transitive(below)
     requires Connected(below)
     modifies a
diff --git a/StandardLibrary/src/StandardLibrary.dfy b/StandardLibrary/src/StandardLibrary.dfy
index 0a29fdb4b..8f263f351 100644
--- a/StandardLibrary/src/StandardLibrary.dfy
+++ b/StandardLibrary/src/StandardLibrary.dfy
@@ -244,7 +244,7 @@ module StandardLibrary {
     assert LexicographicLessOrEqualAux(a, a, less, |a|);
   }
 
-  lemma LexIsAntisymmetric<T>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
+  lemma LexIsAntisymmetric<T(!new)>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
     requires Trich: Trichotomous(less)
     requires LexicographicLessOrEqual(a, b, less)
     requires LexicographicLessOrEqual(b, a, less)
@@ -287,7 +287,7 @@ module StandardLibrary {
     }
   }
 
-  lemma LexIsTransitive<T>(a: seq<T>, b: seq<T>, c: seq<T>, less: (T, T) -> bool)
+  lemma LexIsTransitive<T(!new)>(a: seq<T>, b: seq<T>, c: seq<T>, less: (T, T) -> bool)
     requires Transitive(less)
     requires LexicographicLessOrEqual(a, b, less)
     requires LexicographicLessOrEqual(b, c, less)
@@ -299,7 +299,7 @@ module StandardLibrary {
     assert LexicographicLessOrEqualAux(a, c, less, k);
   }
 
-  lemma LexIsTotal<T>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
+  lemma LexIsTotal<T(!new)>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
     requires Trich: Trichotomous(less)
     ensures LexicographicLessOrEqual(a, b, less) || LexicographicLessOrEqual(b, a, less)
   {
@@ -375,7 +375,7 @@ module StandardLibrary {
     forall z :: z in s ==> LexicographicLessOrEqual(a, z, less)
   }
 
-  lemma ThereIsAMinimum<T>(s: set<seq<T>>, less: (T, T) -> bool)
+  lemma ThereIsAMinimum<T(!new)>(s: set<seq<T>>, less: (T, T) -> bool)
     requires s != {}
     requires Trichotomous(less) && Transitive(less)
     ensures exists a :: IsMinimum(a, s, less)
@@ -383,7 +383,7 @@ module StandardLibrary {
     var a := FindMinimum(s, less);
   }
 
-  lemma MinimumIsUnique<T>(a: seq<T>, b: seq<T>, s: set<seq<T>>, less: (T, T) -> bool)
+  lemma MinimumIsUnique<T(!new)>(a: seq<T>, b: seq<T>, s: set<seq<T>>, less: (T, T) -> bool)
     requires IsMinimum(a, s, less) && IsMinimum(b, s, less)
     requires Trichotomous(less)
     ensures a == b
@@ -391,7 +391,7 @@ module StandardLibrary {
     LexIsAntisymmetric(a, b, less);
   }
 
-  lemma FindMinimum<T>(s: set<seq<T>>, less: (T, T) -> bool) returns (a: seq<T>)
+  lemma FindMinimum<T(!new)>(s: set<seq<T>>, less: (T, T) -> bool) returns (a: seq<T>)
     requires s != {}
     requires Trichotomous(less) && Transitive(less)
     ensures IsMinimum(a, s, less)
diff --git a/libraries b/libraries
index 5d8934326..e9b898d0e 160000
--- a/libraries
+++ b/libraries
@@ -1 +1 @@
-Subproject commit 5d8934326131b8433ce83eac628336b22c15dd58
+Subproject commit e9b898d0ec08e129b8e61306b2617b36c4ce5d3e