diff --git a/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml b/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml
index 133c0713185..e2efd9060f6 100644
--- a/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml
+++ b/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml
@@ -60,10 +60,10 @@ let (embed_nat_int : Prims.nat -> Prims.int) = fun n -> n
 let (uu___0 : (Prims.nat, Prims.int, unit, unit, unit) monoid_morphism) =
   intro_monoid_morphism embed_nat_int nat_plus_monoid int_plus_monoid
 type 'p neg = unit
-let (uu___1 : (unit, unit, unit neg, unit, unit) monoid_morphism) =
+let (uu___1 : (unit, unit, unit, unit, unit) monoid_morphism) =
   intro_monoid_morphism (fun uu___ -> ()) conjunction_monoid
     disjunction_monoid
-let (uu___2 : (unit, unit, unit neg, unit, unit) monoid_morphism) =
+let (uu___2 : (unit, unit, unit, unit, unit) monoid_morphism) =
   intro_monoid_morphism (fun uu___ -> ()) disjunction_monoid
     conjunction_monoid
 type ('m, 'a, 'mult, 'act) mult_act_lemma = unit
diff --git a/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml b/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml
index 1f8425ded08..5ee00f0e445 100644
--- a/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml
+++ b/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml
@@ -9,15 +9,14 @@ let alloc_mref_seq :
   'a .
     unit ->
       'a FStar_Seq_Base.seq ->
-        (unit, 'a FStar_Seq_Base.seq, ('a, unit, unit) grows)
-          FStar_HyperStack_ST.m_rref
+        (unit, 'a FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref
   = fun r -> fun init -> FStar_HyperStack_ST.ralloc () init
 type ('a, 'i, 'n, 'x, 'r, 'h) at_least = unit
 let write_at_end :
   'a .
     unit ->
-      (unit, 'a FStar_Seq_Base.seq, ('a, unit, unit) grows)
-        FStar_HyperStack_ST.m_rref -> 'a -> unit
+      (unit, 'a FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref ->
+        'a -> unit
   =
   fun i ->
     fun r ->
@@ -52,16 +51,15 @@ let i_write_at_end : 'a 'p . unit -> (unit, 'a, 'p) i_seq -> 'a -> unit =
 type 's invariant = unit
 let (test0 :
   unit ->
-    (unit, Prims.nat FStar_Seq_Base.seq, (Prims.nat, unit, unit) grows)
-      FStar_HyperStack_ST.m_rref -> Prims.nat -> unit)
+    (unit, Prims.nat FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref ->
+      Prims.nat -> unit)
   =
   fun r ->
     fun a ->
       fun k ->
         let h0 = FStar_HyperStack_ST.get () in
         FStar_HyperStack_ST.mr_witness () () () (Obj.magic a) ()
-let (itest :
-  unit -> (unit, Prims.nat, unit invariant) i_seq -> Prims.nat -> unit) =
+let (itest : unit -> (unit, Prims.nat, unit) i_seq -> Prims.nat -> unit) =
   fun r ->
     fun a ->
       fun k ->
diff --git a/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml b/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml
index 4aa36833970..43fc68866d2 100644
--- a/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml
+++ b/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml
@@ -37,8 +37,7 @@ let default_wfr : 'a . unit -> 'a wfr_t =
       proof = ()
     }
 type ('a, 'x1, 'x2) empty_relation = unit
-let rec empty_decreaser :
-  'a . 'a -> ('a, ('a, unit, unit) empty_relation, unit) acc_classical =
+let rec empty_decreaser : 'a . 'a -> ('a, unit, unit) acc_classical =
   fun x -> let smaller y = empty_decreaser y in AccClassicalIntro smaller
 let empty_wfr : 'a . unit -> 'a wfr_t =
   fun uu___ ->
@@ -48,9 +47,7 @@ let empty_wfr : 'a . unit -> 'a wfr_t =
       proof = ()
     }
 type ('a, 'r, 'x1, 'x2) acc_relation = unit
-let rec acc_decreaser :
-  'a 'r .
-    unit -> 'a -> ('a, ('a, 'r, unit, unit) acc_relation, unit) acc_classical
+let rec acc_decreaser : 'a 'r . unit -> 'a -> ('a, unit, unit) acc_classical
   =
   fun f ->
     fun x -> let smaller y = acc_decreaser () y in AccClassicalIntro smaller
diff --git a/ocaml/fstar-lib/generated/LowStar_Buffer.ml b/ocaml/fstar-lib/generated/LowStar_Buffer.ml
index 9059a9cc0cc..73d55a5a93f 100644
--- a/ocaml/fstar-lib/generated/LowStar_Buffer.ml
+++ b/ocaml/fstar-lib/generated/LowStar_Buffer.ml
@@ -8,25 +8,15 @@ type 'a pointer_or_null = 'a buffer
 let sub :
   'a .
     unit ->
-      ('a, ('a, unit, unit) trivial_preorder,
-        ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer
-        ->
+      ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer ->
         FStar_UInt32.t ->
-          unit ->
-            ('a, ('a, unit, unit) trivial_preorder,
-              ('a, unit, unit) trivial_preorder)
-              LowStar_Monotonic_Buffer.mbuffer
+          unit -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.msub
 let offset :
   'a .
     unit ->
-      ('a, ('a, unit, unit) trivial_preorder,
-        ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer
-        ->
-        FStar_UInt32.t ->
-          ('a, ('a, unit, unit) trivial_preorder,
-            ('a, unit, unit) trivial_preorder)
-            LowStar_Monotonic_Buffer.mbuffer
+      ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer ->
+        FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.moffset
 type ('a, 'len) lbuffer = ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer
 let gcmalloc :
@@ -34,45 +24,31 @@ let gcmalloc :
     unit ->
       unit ->
         'a ->
-          FStar_UInt32.t ->
-            ('a, ('a, unit, unit) trivial_preorder,
-              ('a, unit, unit) trivial_preorder)
-              LowStar_Monotonic_Buffer.mbuffer
+          FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.mgcmalloc
 let malloc :
   'a .
     unit ->
       unit ->
         'a ->
-          FStar_UInt32.t ->
-            ('a, ('a, unit, unit) trivial_preorder,
-              ('a, unit, unit) trivial_preorder)
-              LowStar_Monotonic_Buffer.mbuffer
+          FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.mmalloc
 let alloca :
   'a .
     unit ->
       'a ->
-        FStar_UInt32.t ->
-          ('a, ('a, unit, unit) trivial_preorder,
-            ('a, unit, unit) trivial_preorder)
-            LowStar_Monotonic_Buffer.mbuffer
+        FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.malloca
 let alloca_of_list :
   'a .
     unit ->
-      'a Prims.list ->
-        ('a, ('a, unit, unit) trivial_preorder,
-          ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer
+      'a Prims.list -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.malloca_of_list
 let gcmalloc_of_list :
   'a .
     unit ->
       unit ->
-        'a Prims.list ->
-          ('a, ('a, unit, unit) trivial_preorder,
-            ('a, unit, unit) trivial_preorder)
-            LowStar_Monotonic_Buffer.mbuffer
+        'a Prims.list -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.mgcmalloc_of_list
 type ('a, 'l) assign_list_t = 'a buffer -> unit
 let rec assign_list : 'a . 'a Prims.list -> 'a buffer -> unit =
diff --git a/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml b/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml
index c0a81fdda4e..648a3cef0f8 100644
--- a/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml
+++ b/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml
@@ -14,10 +14,7 @@ type 'len lbuffer = buffer
 type ('r, 'len) malloc_pre = unit
 type ('h0, 'b, 'h1) alloc_post_mem_common = unit
 let (update_frozen_until_alloc :
-  (u8, (unit, unit) prefix_freezable_preorder,
-    (unit, unit) prefix_freezable_preorder) LowStar_Monotonic_Buffer.mbuffer
-    -> unit)
-  =
+  (u8, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> unit) =
   fun b ->
     LowStar_Endianness.store32_le_i b Stdint.Uint32.zero
       (Stdint.Uint32.of_int (4));
diff --git a/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml b/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml
index 24e8950e216..9a417b88559 100644
--- a/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml
+++ b/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml
@@ -10,28 +10,20 @@ type 'a pointer_or_null = 'a ubuffer
 let usub :
   'a .
     unit ->
-      ('a FStar_Pervasives_Native.option,
-        ('a, unit, unit) initialization_preorder,
-        ('a, unit, unit) initialization_preorder)
+      ('a FStar_Pervasives_Native.option, unit, unit)
         LowStar_Monotonic_Buffer.mbuffer ->
         FStar_UInt32.t ->
           unit ->
-            ('a FStar_Pervasives_Native.option,
-              ('a, unit, unit) initialization_preorder,
-              ('a, unit, unit) initialization_preorder)
+            ('a FStar_Pervasives_Native.option, unit, unit)
               LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.msub
 let uoffset :
   'a .
     unit ->
-      ('a FStar_Pervasives_Native.option,
-        ('a, unit, unit) initialization_preorder,
-        ('a, unit, unit) initialization_preorder)
+      ('a FStar_Pervasives_Native.option, unit, unit)
         LowStar_Monotonic_Buffer.mbuffer ->
         FStar_UInt32.t ->
-          ('a FStar_Pervasives_Native.option,
-            ('a, unit, unit) initialization_preorder,
-            ('a, unit, unit) initialization_preorder)
+          ('a FStar_Pervasives_Native.option, unit, unit)
             LowStar_Monotonic_Buffer.mbuffer
   = fun uu___ -> LowStar_Monotonic_Buffer.moffset
 type ('a, 'i, 's) ipred = unit