Improve the generation of variant names for Lean

14 files changed, 452 insertions, 466 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index f2b5f00f..476359f0 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -915,8 +915,10 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
 
      Note that we already printed: [type s =]
   *)
-  let print_variant variant_id v =
-    let cons_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in
+  let print_variant _variant_id (v : variant) =
+    (* We don't lookup the name, because it may have a prefix for the type
+       id (in the case of Lean) *)
+    let cons_name = ctx.fmt.variant_name def.name v.variant_name in
     let fields = v.fields in
     extract_type_decl_variant ctx fmt def_name type_params cons_name fields
   in
@@ -1535,12 +1537,14 @@ let extract_adt_g_value
         (* The ADT shouldn't be opaque *)
         let with_opaque_pre = false in
         match variant_id with
-        | Some vid ->
-            if !backend = Lean then
-              ctx_get_type with_opaque_pre adt_id ctx
-              ^ "."
-              ^ ctx_get_variant adt_id vid ctx
-            else ctx_get_variant adt_id vid ctx
+        | Some vid -> (
+            (* In the case of Lean, we might have to add the type name as a prefix *)
+            match (!backend, adt_id) with
+            | Lean, Assumed _ ->
+                ctx_get_type with_opaque_pre adt_id ctx
+                ^ "."
+                ^ ctx_get_variant adt_id vid ctx
+            | _ -> ctx_get_variant adt_id vid ctx)
         | None -> ctx_get_struct with_opaque_pre adt_id ctx
       in
       if inside && field_values <> [] then F.pp_print_string fmt "(";
@@ -1731,6 +1735,7 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
           args;
         F.pp_print_string fmt ")")
   | _ ->
+      (* TODO: this duplicates [extrac_adt_g_value] *)
       (* "Regular" ADT *)
       (* We print something of the form: [Cons field0 ... fieldn].
        * We could update the code to print something of the form:
@@ -1741,12 +1746,14 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         (* The ADT shouldn't be opaque *)
         let with_opaque_pre = false in
         match adt_cons.variant_id with
-        | Some vid ->
-            if !backend = Lean then
-              ctx_get_type with_opaque_pre adt_cons.adt_id ctx
-              ^ "."
-              ^ ctx_get_variant adt_cons.adt_id vid ctx
-            else ctx_get_variant adt_cons.adt_id vid ctx
+        | Some vid -> (
+            (* In the case of Lean, we might have to add the type name as a prefix *)
+            match (!backend, adt_cons.adt_id) with
+            | Lean, Assumed _ ->
+                ctx_get_type with_opaque_pre adt_cons.adt_id ctx
+                ^ "."
+                ^ ctx_get_variant adt_cons.adt_id vid ctx
+            | _ -> ctx_get_variant adt_cons.adt_id vid ctx)
         | None -> ctx_get_struct with_opaque_pre adt_cons.adt_id ctx
       in
       let use_parentheses = inside && args <> [] in
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 86bb0cff..81bdd202 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -805,6 +805,13 @@ let ctx_add_variant (def : type_decl) (variant_id : VariantId.id)
     (variant : variant) (ctx : extraction_ctx) : extraction_ctx * string =
   let is_opaque = false in
   let name = ctx.fmt.variant_name def.name variant.variant_name in
+  (* Add the type name prefix for Lean *)
+  let name =
+    if !Config.backend = Lean then
+      let type_name = ctx.fmt.type_name def.name in
+      type_name ^ "." ^ name
+    else name
+  in
   let ctx =
     ctx_add is_opaque (VariantId (AdtId def.def_id, variant_id)) name ctx
   in
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 347052a8..781766ee 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -796,7 +796,11 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   (* Initialize the extraction context - for now we extract only to F*.
    * We initialize the names map by registering the keywords used in the
    * language, as well as some primitive names ("u32", etc.) *)
-  let variant_concatenate_type_name = true in
+  let variant_concatenate_type_name =
+    (* For Lean, we exploit the fact that the variant name should always be
+       prefixed with the type name to prevent collisions *)
+    match !Config.backend with Coq | FStar -> true | Lean -> false
+  in
   let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in
   let fmt, names_map =
     mk_formatter_and_names_map trans_ctx crate.name
diff --git a/tests/lean/betree/BetreeMain/Funs.lean b/tests/lean/betree/BetreeMain/Funs.lean
index e161e066..7177e2ec 100644
--- a/tests/lean/betree/BetreeMain/Funs.lean
+++ b/tests/lean/betree/BetreeMain/Funs.lean
@@ -83,18 +83,18 @@ def betree_upsert_update_fwd
   match h: prev with
   | Option.none =>
     match h: st with
-    | betree_upsert_fun_state_t.BetreeUpsertFunStateAdd v => Result.ret v
-    | betree_upsert_fun_state_t.BetreeUpsertFunStateSub i =>
+    | betree_upsert_fun_state_t.Add v => Result.ret v
+    | betree_upsert_fun_state_t.Sub i =>
       Result.ret (UInt64.ofNatCore 0 (by intlit))
   | Option.some prev0 =>
     match h: st with
-    | betree_upsert_fun_state_t.BetreeUpsertFunStateAdd v =>
+    | betree_upsert_fun_state_t.Add v =>
       do
         let margin ← UInt64.checked_sub core_num_u64_max_c prev0
         if h: margin >= v
         then UInt64.checked_add prev0 v
         else Result.ret core_num_u64_max_c
-    | betree_upsert_fun_state_t.BetreeUpsertFunStateSub v =>
+    | betree_upsert_fun_state_t.Sub v =>
       if h: prev0 >= v
       then UInt64.checked_sub prev0 v
       else Result.ret (UInt64.ofNatCore 0 (by intlit))
@@ -103,11 +103,11 @@ def betree_upsert_update_fwd
 def betree_list_len_fwd
   (T : Type) (self : betree_list_t T) : (Result UInt64) :=
   match h: self with
-  | betree_list_t.BetreeListCons t tl =>
+  | betree_list_t.Cons t tl =>
     do
       let i ← betree_list_len_fwd T tl
       UInt64.checked_add (UInt64.ofNatCore 1 (by intlit)) i
-  | betree_list_t.BetreeListNil => Result.ret (UInt64.ofNatCore 0 (by intlit))
+  | betree_list_t.Nil => Result.ret (UInt64.ofNatCore 0 (by intlit))
 termination_by betree_list_len_fwd self => betree_list_len_terminates T self
 decreasing_by betree_list_len_decreases self
 
@@ -117,17 +117,17 @@ def betree_list_split_at_fwd
   (Result ((betree_list_t T) × (betree_list_t T)))
   :=
   if h: n = (UInt64.ofNatCore 0 (by intlit))
-  then Result.ret (betree_list_t.BetreeListNil, self)
+  then Result.ret (betree_list_t.Nil, self)
   else
     match h: self with
-    | betree_list_t.BetreeListCons hd tl =>
+    | betree_list_t.Cons hd tl =>
       do
         let i ← UInt64.checked_sub n (UInt64.ofNatCore 1 (by intlit))
         let p ← betree_list_split_at_fwd T tl i
         let (ls0, ls1) := p
         let l := ls0
-        Result.ret (betree_list_t.BetreeListCons hd l, ls1)
-    | betree_list_t.BetreeListNil => Result.fail Error.panic
+        Result.ret (betree_list_t.Cons hd l, ls1)
+    | betree_list_t.Nil => Result.fail Error.panic
 termination_by betree_list_split_at_fwd self n =>
   betree_list_split_at_terminates T self n
 decreasing_by betree_list_split_at_decreases self n
@@ -135,30 +135,30 @@ decreasing_by betree_list_split_at_decreases self n
 /- [betree_main::betree::List::{1}::push_front] -/
 def betree_list_push_front_fwd_back
   (T : Type) (self : betree_list_t T) (x : T) : Result (betree_list_t T) :=
-  let tl := mem_replace_fwd (betree_list_t T) self betree_list_t.BetreeListNil
+  let tl := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
   let l := tl
-  Result.ret (betree_list_t.BetreeListCons x l)
+  Result.ret (betree_list_t.Cons x l)
 
 /- [betree_main::betree::List::{1}::pop_front] -/
 def betree_list_pop_front_fwd (T : Type) (self : betree_list_t T) : Result T :=
-  let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.BetreeListNil
+  let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
   match h: ls with
-  | betree_list_t.BetreeListCons x tl => Result.ret x
-  | betree_list_t.BetreeListNil => Result.fail Error.panic
+  | betree_list_t.Cons x tl => Result.ret x
+  | betree_list_t.Nil => Result.fail Error.panic
 
 /- [betree_main::betree::List::{1}::pop_front] -/
 def betree_list_pop_front_back
   (T : Type) (self : betree_list_t T) : Result (betree_list_t T) :=
-  let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.BetreeListNil
+  let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
   match h: ls with
-  | betree_list_t.BetreeListCons x tl => Result.ret tl
-  | betree_list_t.BetreeListNil => Result.fail Error.panic
+  | betree_list_t.Cons x tl => Result.ret tl
+  | betree_list_t.Nil => Result.fail Error.panic
 
 /- [betree_main::betree::List::{1}::hd] -/
 def betree_list_hd_fwd (T : Type) (self : betree_list_t T) : Result T :=
   match h: self with
-  | betree_list_t.BetreeListCons hd l => Result.ret hd
-  | betree_list_t.BetreeListNil => Result.fail Error.panic
+  | betree_list_t.Cons hd l => Result.ret hd
+  | betree_list_t.Nil => Result.fail Error.panic
 
 /- [betree_main::betree::List::{2}::head_has_key] -/
 def betree_list_head_has_key_fwd
@@ -166,9 +166,9 @@ def betree_list_head_has_key_fwd
   Result Bool
   :=
   match h: self with
-  | betree_list_t.BetreeListCons hd l => let (i, _) := hd
-                                         Result.ret (i = key)
-  | betree_list_t.BetreeListNil => Result.ret false
+  | betree_list_t.Cons hd l => let (i, _) := hd
+                               Result.ret (i = key)
+  | betree_list_t.Nil => Result.ret false
 
 /- [betree_main::betree::List::{2}::partition_at_pivot] -/
 def betree_list_partition_at_pivot_fwd
@@ -176,20 +176,17 @@ def betree_list_partition_at_pivot_fwd
   (Result ((betree_list_t (UInt64 × T)) × (betree_list_t (UInt64 × T))))
   :=
   match h: self with
-  | betree_list_t.BetreeListCons hd tl =>
+  | betree_list_t.Cons hd tl =>
     let (i, t) := hd
     if h: i >= pivot
-    then
-      Result.ret (betree_list_t.BetreeListNil, betree_list_t.BetreeListCons (i,
-        t) tl)
+    then Result.ret (betree_list_t.Nil, betree_list_t.Cons (i, t) tl)
     else
       do
         let p ← betree_list_partition_at_pivot_fwd T tl pivot
         let (ls0, ls1) := p
         let l := ls0
-        Result.ret (betree_list_t.BetreeListCons (i, t) l, ls1)
-  | betree_list_t.BetreeListNil =>
-    Result.ret (betree_list_t.BetreeListNil, betree_list_t.BetreeListNil)
+        Result.ret (betree_list_t.Cons (i, t) l, ls1)
+  | betree_list_t.Nil => Result.ret (betree_list_t.Nil, betree_list_t.Nil)
 termination_by betree_list_partition_at_pivot_fwd self pivot =>
   betree_list_partition_at_pivot_terminates T self pivot
 decreasing_by betree_list_partition_at_pivot_decreases self pivot
@@ -213,12 +210,12 @@ def betree_leaf_split_fwd
     let id1 ← betree_node_id_counter_fresh_id_fwd node_id_cnt0
     let (st0, _) ← betree_store_leaf_node_fwd id0 content0 st
     let (st1, _) ← betree_store_leaf_node_fwd id1 content1 st0
-    let n := betree_node_t.BetreeNodeLeaf
+    let n := betree_node_t.Leaf
       {
         betree_leaf_id := id0,
         betree_leaf_size := params.betree_params_split_size
       }
-    let n0 := betree_node_t.BetreeNodeLeaf
+    let n0 := betree_node_t.Leaf
       {
         betree_leaf_id := id1,
         betree_leaf_size := params.betree_params_split_size
@@ -251,7 +248,7 @@ def betree_node_lookup_in_bindings_fwd
   (Result (Option UInt64))
   :=
   match h: bindings with
-  | betree_list_t.BetreeListCons hd tl =>
+  | betree_list_t.Cons hd tl =>
     let (i, i0) := hd
     if h: i = key
     then Result.ret (Option.some i0)
@@ -259,7 +256,7 @@ def betree_node_lookup_in_bindings_fwd
       if h: i > key
       then Result.ret Option.none
       else betree_node_lookup_in_bindings_fwd key tl
-  | betree_list_t.BetreeListNil => Result.ret Option.none
+  | betree_list_t.Nil => Result.ret Option.none
 termination_by betree_node_lookup_in_bindings_fwd key bindings =>
   betree_node_lookup_in_bindings_terminates key bindings
 decreasing_by betree_node_lookup_in_bindings_decreases key bindings
@@ -270,12 +267,12 @@ def betree_node_lookup_first_message_for_key_fwd
   (Result (betree_list_t (UInt64 × betree_message_t)))
   :=
   match h: msgs with
-  | betree_list_t.BetreeListCons x next_msgs =>
+  | betree_list_t.Cons x next_msgs =>
     let (i, m) := x
     if h: i >= key
-    then Result.ret (betree_list_t.BetreeListCons (i, m) next_msgs)
+    then Result.ret (betree_list_t.Cons (i, m) next_msgs)
     else betree_node_lookup_first_message_for_key_fwd key next_msgs
-  | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil
+  | betree_list_t.Nil => Result.ret betree_list_t.Nil
 termination_by betree_node_lookup_first_message_for_key_fwd key msgs =>
   betree_node_lookup_first_message_for_key_terminates key msgs
 decreasing_by betree_node_lookup_first_message_for_key_decreases key msgs
@@ -287,7 +284,7 @@ def betree_node_lookup_first_message_for_key_back
   (Result (betree_list_t (UInt64 × betree_message_t)))
   :=
   match h: msgs with
-  | betree_list_t.BetreeListCons x next_msgs =>
+  | betree_list_t.Cons x next_msgs =>
     let (i, m) := x
     if h: i >= key
     then Result.ret ret0
@@ -295,8 +292,8 @@ def betree_node_lookup_first_message_for_key_back
       do
         let next_msgs0 ←
           betree_node_lookup_first_message_for_key_back key next_msgs ret0
-        Result.ret (betree_list_t.BetreeListCons (i, m) next_msgs0)
-  | betree_list_t.BetreeListNil => Result.ret ret0
+        Result.ret (betree_list_t.Cons (i, m) next_msgs0)
+  | betree_list_t.Nil => Result.ret ret0
 termination_by betree_node_lookup_first_message_for_key_back key msgs ret0 =>
   betree_node_lookup_first_message_for_key_terminates key msgs
 decreasing_by betree_node_lookup_first_message_for_key_decreases key msgs
@@ -315,9 +312,9 @@ def betree_node_apply_upserts_fwd
         let msg ← betree_list_pop_front_fwd (UInt64 × betree_message_t) msgs
         let (_, m) := msg
         match h: m with
-        | betree_message_t.BetreeMessageInsert i => Result.fail Error.panic
-        | betree_message_t.BetreeMessageDelete => Result.fail Error.panic
-        | betree_message_t.BetreeMessageUpsert s =>
+        | betree_message_t.Insert i => Result.fail Error.panic
+        | betree_message_t.Delete => Result.fail Error.panic
+        | betree_message_t.Upsert s =>
           do
             let v ← betree_upsert_update_fwd prev s
             let msgs0 ←
@@ -329,7 +326,7 @@ def betree_node_apply_upserts_fwd
           opaque_defs.core_option_option_unwrap_fwd UInt64 prev st
         let _ ←
           betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs
-            (key, betree_message_t.BetreeMessageInsert v)
+            (key, betree_message_t.Insert v)
         Result.ret (st0, v)
 termination_by betree_node_apply_upserts_fwd msgs prev key st =>
   betree_node_apply_upserts_terminates msgs prev key st
@@ -349,9 +346,9 @@ def betree_node_apply_upserts_back
         let msg ← betree_list_pop_front_fwd (UInt64 × betree_message_t) msgs
         let (_, m) := msg
         match h: m with
-        | betree_message_t.BetreeMessageInsert i => Result.fail Error.panic
-        | betree_message_t.BetreeMessageDelete => Result.fail Error.panic
-        | betree_message_t.BetreeMessageUpsert s =>
+        | betree_message_t.Insert i => Result.fail Error.panic
+        | betree_message_t.Delete => Result.fail Error.panic
+        | betree_message_t.Upsert s =>
           do
             let v ← betree_upsert_update_fwd prev s
             let msgs0 ←
@@ -361,7 +358,7 @@ def betree_node_apply_upserts_back
       do
         let (_, v) ← opaque_defs.core_option_option_unwrap_fwd UInt64 prev st
         betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs (key,
-          betree_message_t.BetreeMessageInsert v)
+          betree_message_t.Insert v)
 termination_by betree_node_apply_upserts_back msgs prev key st =>
   betree_node_apply_upserts_terminates msgs prev key st
 decreasing_by betree_node_apply_upserts_decreases msgs prev key st
@@ -372,13 +369,13 @@ mutual def betree_node_lookup_fwd
   (Result (State × (Option UInt64)))
   :=
   match h: self with
-  | betree_node_t.BetreeNodeInternal node =>
+  | betree_node_t.Internal node =>
     do
       let (mkbetree_internal_t i i0 n n0) := node
       let (st0, msgs) ← betree_load_internal_node_fwd i st
       let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
       match h: pending with
-      | betree_list_t.BetreeListCons p l =>
+      | betree_list_t.Cons p l =>
         let (k, msg) := p
         if h: k != key
         then
@@ -388,53 +385,51 @@ mutual def betree_node_lookup_fwd
                 n n0) key st0
             let _ ←
               betree_node_lookup_first_message_for_key_back key msgs
-                (betree_list_t.BetreeListCons (k, msg) l)
+                (betree_list_t.Cons (k, msg) l)
             Result.ret (st1, opt)
         else
           match h: msg with
-          | betree_message_t.BetreeMessageInsert v =>
+          | betree_message_t.Insert v =>
             do
               let _ ←
                 betree_node_lookup_first_message_for_key_back key msgs
-                  (betree_list_t.BetreeListCons (k,
-                  betree_message_t.BetreeMessageInsert v) l)
+                  (betree_list_t.Cons (k, betree_message_t.Insert v) l)
               Result.ret (st0, Option.some v)
-          | betree_message_t.BetreeMessageDelete =>
+          | betree_message_t.Delete =>
             do
               let _ ←
                 betree_node_lookup_first_message_for_key_back key msgs
-                  (betree_list_t.BetreeListCons (k,
-                  betree_message_t.BetreeMessageDelete) l)
+                  (betree_list_t.Cons (k, betree_message_t.Delete) l)
               Result.ret (st0, Option.none)
-          | betree_message_t.BetreeMessageUpsert ufs =>
+          | betree_message_t.Upsert ufs =>
             do
               let (st1, v) ←
                 betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
                   i0 n n0) key st0
               let (st2, v0) ←
-                betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k,
-                  betree_message_t.BetreeMessageUpsert ufs) l) v key st1
+                betree_node_apply_upserts_fwd (betree_list_t.Cons (k,
+                  betree_message_t.Upsert ufs) l) v key st1
               let node0 ←
                 betree_internal_lookup_in_children_back (mkbetree_internal_t i
                   i0 n n0) key st0
               let (mkbetree_internal_t i1 _ _ _) := node0
               let pending0 ←
-                betree_node_apply_upserts_back (betree_list_t.BetreeListCons
-                  (k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1
+                betree_node_apply_upserts_back (betree_list_t.Cons (k,
+                  betree_message_t.Upsert ufs) l) v key st1
               let msgs0 ←
                 betree_node_lookup_first_message_for_key_back key msgs pending0
               let (st3, _) ← betree_store_internal_node_fwd i1 msgs0 st2
               Result.ret (st3, Option.some v0)
-      | betree_list_t.BetreeListNil =>
+      | betree_list_t.Nil =>
         do
           let (st1, opt) ←
             betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n
               n0) key st0
           let _ ←
             betree_node_lookup_first_message_for_key_back key msgs
-              betree_list_t.BetreeListNil
+              betree_list_t.Nil
           Result.ret (st1, opt)
-  | betree_node_t.BetreeNodeLeaf node =>
+  | betree_node_t.Leaf node =>
     do
       let (st0, bindings) ← betree_load_leaf_node_fwd node.betree_leaf_id st
       let opt ← betree_node_lookup_in_bindings_fwd key bindings
@@ -449,76 +444,74 @@ def betree_node_lookup_back
   (Result betree_node_t)
   :=
   match h: self with
-  | betree_node_t.BetreeNodeInternal node =>
+  | betree_node_t.Internal node =>
     do
       let (mkbetree_internal_t i i0 n n0) := node
       let (st0, msgs) ← betree_load_internal_node_fwd i st
       let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
       match h: pending with
-      | betree_list_t.BetreeListCons p l =>
+      | betree_list_t.Cons p l =>
         let (k, msg) := p
         if h: k != key
         then
           do
             let _ ←
               betree_node_lookup_first_message_for_key_back key msgs
-                (betree_list_t.BetreeListCons (k, msg) l)
+                (betree_list_t.Cons (k, msg) l)
             let node0 ←
               betree_internal_lookup_in_children_back (mkbetree_internal_t i i0
                 n n0) key st0
-            Result.ret (betree_node_t.BetreeNodeInternal node0)
+            Result.ret (betree_node_t.Internal node0)
         else
           match h: msg with
-          | betree_message_t.BetreeMessageInsert v =>
+          | betree_message_t.Insert v =>
             do
               let _ ←
                 betree_node_lookup_first_message_for_key_back key msgs
-                  (betree_list_t.BetreeListCons (k,
-                  betree_message_t.BetreeMessageInsert v) l)
-              Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
-                i i0 n n0))
-          | betree_message_t.BetreeMessageDelete =>
+                  (betree_list_t.Cons (k, betree_message_t.Insert v) l)
+              Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n
+                n0))
+          | betree_message_t.Delete =>
             do
               let _ ←
                 betree_node_lookup_first_message_for_key_back key msgs
-                  (betree_list_t.BetreeListCons (k,
-                  betree_message_t.BetreeMessageDelete) l)
-              Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
-                i i0 n n0))
-          | betree_message_t.BetreeMessageUpsert ufs =>
+                  (betree_list_t.Cons (k, betree_message_t.Delete) l)
+              Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n
+                n0))
+          | betree_message_t.Upsert ufs =>
             do
               let (st1, v) ←
                 betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
                   i0 n n0) key st0
               let (st2, _) ←
-                betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k,
-                  betree_message_t.BetreeMessageUpsert ufs) l) v key st1
+                betree_node_apply_upserts_fwd (betree_list_t.Cons (k,
+                  betree_message_t.Upsert ufs) l) v key st1
               let node0 ←
                 betree_internal_lookup_in_children_back (mkbetree_internal_t i
                   i0 n n0) key st0
               let (mkbetree_internal_t i1 i2 n1 n2) := node0
               let pending0 ←
-                betree_node_apply_upserts_back (betree_list_t.BetreeListCons
-                  (k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1
+                betree_node_apply_upserts_back (betree_list_t.Cons (k,
+                  betree_message_t.Upsert ufs) l) v key st1
               let msgs0 ←
                 betree_node_lookup_first_message_for_key_back key msgs pending0
               let _ ← betree_store_internal_node_fwd i1 msgs0 st2
-              Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t
-                i1 i2 n1 n2))
-      | betree_list_t.BetreeListNil =>
+              Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1
+                n2))
+      | betree_list_t.Nil =>
         do
           let _ ←
             betree_node_lookup_first_message_for_key_back key msgs
-              betree_list_t.BetreeListNil
+              betree_list_t.Nil
           let node0 ←
             betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n
               n0) key st0
-          Result.ret (betree_node_t.BetreeNodeInternal node0)
-  | betree_node_t.BetreeNodeLeaf node =>
+          Result.ret (betree_node_t.Internal node0)
+  | betree_node_t.Leaf node =>
     do
       let (_, bindings) ← betree_load_leaf_node_fwd node.betree_leaf_id st
       let _ ← betree_node_lookup_in_bindings_fwd key bindings
-      Result.ret (betree_node_t.BetreeNodeLeaf node)
+      Result.ret (betree_node_t.Leaf node)
 termination_by betree_node_lookup_back self key st =>
   betree_node_lookup_terminates self key st
 decreasing_by betree_node_lookup_decreases self key st
@@ -561,12 +554,12 @@ def betree_node_lookup_mut_in_bindings_fwd
   (Result (betree_list_t (UInt64 × UInt64)))
   :=
   match h: bindings with
-  | betree_list_t.BetreeListCons hd tl =>
+  | betree_list_t.Cons hd tl =>
     let (i, i0) := hd
     if h: i >= key
-    then Result.ret (betree_list_t.BetreeListCons (i, i0) tl)
+    then Result.ret (betree_list_t.Cons (i, i0) tl)
     else betree_node_lookup_mut_in_bindings_fwd key tl
-  | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil
+  | betree_list_t.Nil => Result.ret betree_list_t.Nil
 termination_by betree_node_lookup_mut_in_bindings_fwd key bindings =>
   betree_node_lookup_mut_in_bindings_terminates key bindings
 decreasing_by betree_node_lookup_mut_in_bindings_decreases key bindings
@@ -578,15 +571,15 @@ def betree_node_lookup_mut_in_bindings_back
   (Result (betree_list_t (UInt64 × UInt64)))
   :=
   match h: bindings with
-  | betree_list_t.BetreeListCons hd tl =>
+  | betree_list_t.Cons hd tl =>
     let (i, i0) := hd
     if h: i >= key
     then Result.ret ret0
     else
       do
         let tl0 ← betree_node_lookup_mut_in_bindings_back key tl ret0
-        Result.ret (betree_list_t.BetreeListCons (i, i0) tl0)
-  | betree_list_t.BetreeListNil => Result.ret ret0
+        Result.ret (betree_list_t.Cons (i, i0) tl0)
+  | betree_list_t.Nil => Result.ret ret0
 termination_by betree_node_lookup_mut_in_bindings_back key bindings ret0 =>
   betree_node_lookup_mut_in_bindings_terminates key bindings
 decreasing_by betree_node_lookup_mut_in_bindings_decreases key bindings
@@ -605,7 +598,7 @@ def betree_node_apply_to_leaf_fwd_back
       do
         let hd ← betree_list_pop_front_fwd (UInt64 × UInt64) bindings0
         match h: new_msg with
-        | betree_message_t.BetreeMessageInsert v =>
+        | betree_message_t.Insert v =>
           do
             let bindings1 ←
               betree_list_pop_front_back (UInt64 × UInt64) bindings0
@@ -613,12 +606,12 @@ def betree_node_apply_to_leaf_fwd_back
               betree_list_push_front_fwd_back (UInt64 × UInt64) bindings1
                 (key, v)
             betree_node_lookup_mut_in_bindings_back key bindings bindings2
-        | betree_message_t.BetreeMessageDelete =>
+        | betree_message_t.Delete =>
           do
             let bindings1 ←
               betree_list_pop_front_back (UInt64 × UInt64) bindings0
             betree_node_lookup_mut_in_bindings_back key bindings bindings1
-        | betree_message_t.BetreeMessageUpsert s =>
+        | betree_message_t.Upsert s =>
           do
             let (_, i) := hd
             let v ← betree_upsert_update_fwd (Option.some i) s
@@ -630,15 +623,15 @@ def betree_node_apply_to_leaf_fwd_back
             betree_node_lookup_mut_in_bindings_back key bindings bindings2
     else
       match h: new_msg with
-      | betree_message_t.BetreeMessageInsert v =>
+      | betree_message_t.Insert v =>
         do
           let bindings1 ←
             betree_list_push_front_fwd_back (UInt64 × UInt64) bindings0 (key,
               v)
           betree_node_lookup_mut_in_bindings_back key bindings bindings1
-      | betree_message_t.BetreeMessageDelete =>
+      | betree_message_t.Delete =>
         betree_node_lookup_mut_in_bindings_back key bindings bindings0
-      | betree_message_t.BetreeMessageUpsert s =>
+      | betree_message_t.Upsert s =>
         do
           let v ← betree_upsert_update_fwd Option.none s
           let bindings1 ←
@@ -653,12 +646,12 @@ def betree_node_apply_messages_to_leaf_fwd_back
   (Result (betree_list_t (UInt64 × UInt64)))
   :=
   match h: new_msgs with
-  | betree_list_t.BetreeListCons new_msg new_msgs_tl =>
+  | betree_list_t.Cons new_msg new_msgs_tl =>
     do
       let (i, m) := new_msg
       let bindings0 ← betree_node_apply_to_leaf_fwd_back bindings i m
       betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
-  | betree_list_t.BetreeListNil => Result.ret bindings
+  | betree_list_t.Nil => Result.ret bindings
 termination_by betree_node_apply_messages_to_leaf_fwd_back bindings new_msgs =>
   betree_node_apply_messages_to_leaf_terminates bindings new_msgs
 decreasing_by betree_node_apply_messages_to_leaf_decreases bindings new_msgs
@@ -669,17 +662,17 @@ def betree_node_filter_messages_for_key_fwd_back
   (Result (betree_list_t (UInt64 × betree_message_t)))
   :=
   match h: msgs with
-  | betree_list_t.BetreeListCons p l =>
+  | betree_list_t.Cons p l =>
     let (k, m) := p
     if h: k = key
     then
       do
         let msgs0 ←
           betree_list_pop_front_back (UInt64 × betree_message_t)
-            (betree_list_t.BetreeListCons (k, m) l)
+            (betree_list_t.Cons (k, m) l)
         betree_node_filter_messages_for_key_fwd_back key msgs0
-    else Result.ret (betree_list_t.BetreeListCons (k, m) l)
-  | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil
+    else Result.ret (betree_list_t.Cons (k, m) l)
+  | betree_list_t.Nil => Result.ret betree_list_t.Nil
 termination_by betree_node_filter_messages_for_key_fwd_back key msgs =>
   betree_node_filter_messages_for_key_terminates key msgs
 decreasing_by betree_node_filter_messages_for_key_decreases key msgs
@@ -690,12 +683,12 @@ def betree_node_lookup_first_message_after_key_fwd
   (Result (betree_list_t (UInt64 × betree_message_t)))
   :=
   match h: msgs with
-  | betree_list_t.BetreeListCons p next_msgs =>
+  | betree_list_t.Cons p next_msgs =>
     let (k, m) := p
     if h: k = key
     then betree_node_lookup_first_message_after_key_fwd key next_msgs
-    else Result.ret (betree_list_t.BetreeListCons (k, m) next_msgs)
-  | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil
+    else Result.ret (betree_list_t.Cons (k, m) next_msgs)
+  | betree_list_t.Nil => Result.ret betree_list_t.Nil
 termination_by betree_node_lookup_first_message_after_key_fwd key msgs =>
   betree_node_lookup_first_message_after_key_terminates key msgs
 decreasing_by betree_node_lookup_first_message_after_key_decreases key msgs
@@ -707,16 +700,16 @@ def betree_node_lookup_first_message_after_key_back
   (Result (betree_list_t (UInt64 × betree_message_t)))
   :=
   match h: msgs with
-  | betree_list_t.BetreeListCons p next_msgs =>
+  | betree_list_t.Cons p next_msgs =>
     let (k, m) := p
     if h: k = key
     then
       do
         let next_msgs0 ←
           betree_node_lookup_first_message_after_key_back key next_msgs ret0
-        Result.ret (betree_list_t.BetreeListCons (k, m) next_msgs0)
+        Result.ret (betree_list_t.Cons (k, m) next_msgs0)
     else Result.ret ret0
-  | betree_list_t.BetreeListNil => Result.ret ret0
+  | betree_list_t.Nil => Result.ret ret0
 termination_by betree_node_lookup_first_message_after_key_back key msgs ret0 =>
   betree_node_lookup_first_message_after_key_terminates key msgs
 decreasing_by betree_node_lookup_first_message_after_key_decreases key msgs
@@ -733,50 +726,50 @@ def betree_node_apply_to_internal_fwd_back
     if h: b
     then
       match h: new_msg with
-      | betree_message_t.BetreeMessageInsert i =>
+      | betree_message_t.Insert i =>
         do
           let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0
           let msgs2 ←
             betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs1
-              (key, betree_message_t.BetreeMessageInsert i)
+              (key, betree_message_t.Insert i)
           betree_node_lookup_first_message_for_key_back key msgs msgs2
-      | betree_message_t.BetreeMessageDelete =>
+      | betree_message_t.Delete =>
         do
           let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0
           let msgs2 ←
             betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs1
-              (key, betree_message_t.BetreeMessageDelete)
+              (key, betree_message_t.Delete)
           betree_node_lookup_first_message_for_key_back key msgs msgs2
-      | betree_message_t.BetreeMessageUpsert s =>
+      | betree_message_t.Upsert s =>
         do
           let p ← betree_list_hd_fwd (UInt64 × betree_message_t) msgs0
           let (_, m) := p
           match h: m with
-          | betree_message_t.BetreeMessageInsert prev =>
+          | betree_message_t.Insert prev =>
             do
               let v ← betree_upsert_update_fwd (Option.some prev) s
               let msgs1 ←
                 betree_list_pop_front_back (UInt64 × betree_message_t) msgs0
               let msgs2 ←
                 betree_list_push_front_fwd_back (UInt64 × betree_message_t)
-                  msgs1 (key, betree_message_t.BetreeMessageInsert v)
+                  msgs1 (key, betree_message_t.Insert v)
               betree_node_lookup_first_message_for_key_back key msgs msgs2
-          | betree_message_t.BetreeMessageDelete =>
+          | betree_message_t.Delete =>
             do
               let v ← betree_upsert_update_fwd Option.none s
               let msgs1 ←
                 betree_list_pop_front_back (UInt64 × betree_message_t) msgs0
               let msgs2 ←
                 betree_list_push_front_fwd_back (UInt64 × betree_message_t)
-                  msgs1 (key, betree_message_t.BetreeMessageInsert v)
+                  msgs1 (key, betree_message_t.Insert v)
               betree_node_lookup_first_message_for_key_back key msgs msgs2
-          | betree_message_t.BetreeMessageUpsert ufs =>
+          | betree_message_t.Upsert ufs =>
             do
               let msgs1 ←
                 betree_node_lookup_first_message_after_key_fwd key msgs0
               let msgs2 ←
                 betree_list_push_front_fwd_back (UInt64 × betree_message_t)
-                  msgs1 (key, betree_message_t.BetreeMessageUpsert s)
+                  msgs1 (key, betree_message_t.Upsert s)
               let msgs3 ←
                 betree_node_lookup_first_message_after_key_back key msgs0 msgs2
               betree_node_lookup_first_message_for_key_back key msgs msgs3
@@ -794,12 +787,12 @@ def betree_node_apply_messages_to_internal_fwd_back
   (Result (betree_list_t (UInt64 × betree_message_t)))
   :=
   match h: new_msgs with
-  | betree_list_t.BetreeListCons new_msg new_msgs_tl =>
+  | betree_list_t.Cons new_msg new_msgs_tl =>
     do
       let (i, m) := new_msg
       let msgs0 ← betree_node_apply_to_internal_fwd_back msgs i m
       betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl
-  | betree_list_t.BetreeListNil => Result.ret msgs
+  | betree_list_t.Nil => Result.ret msgs
 termination_by betree_node_apply_messages_to_internal_fwd_back msgs new_msgs =>
   betree_node_apply_messages_to_internal_terminates msgs new_msgs
 decreasing_by betree_node_apply_messages_to_internal_decreases msgs new_msgs
@@ -812,7 +805,7 @@ mutual def betree_node_apply_messages_fwd
   (Result (State × Unit))
   :=
   match h: self with
-  | betree_node_t.BetreeNodeInternal node =>
+  | betree_node_t.Internal node =>
     do
       let (mkbetree_internal_t i i0 n n0) := node
       let (st0, content) ← betree_load_internal_node_fwd i st
@@ -836,7 +829,7 @@ mutual def betree_node_apply_messages_fwd
         do
           let (st1, _) ← betree_store_internal_node_fwd i content0 st0
           Result.ret (st1, ())
-  | betree_node_t.BetreeNodeLeaf node =>
+  | betree_node_t.Leaf node =>
     do
       let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st
       let content0 ← betree_node_apply_messages_to_leaf_fwd_back content msgs
@@ -849,8 +842,8 @@ mutual def betree_node_apply_messages_fwd
           let (st1, _) ←
             betree_leaf_split_fwd node content0 params node_id_cnt st0
           let (st2, _) ←
-            betree_store_leaf_node_fwd node.betree_leaf_id
-              betree_list_t.BetreeListNil st1
+            betree_store_leaf_node_fwd node.betree_leaf_id betree_list_t.Nil
+              st1
           Result.ret (st2, ())
       else
         do
@@ -871,7 +864,7 @@ def betree_node_apply_messages_back
   (Result (betree_node_t × betree_node_id_counter_t))
   :=
   match h: self with
-  | betree_node_t.BetreeNodeInternal node =>
+  | betree_node_t.Internal node =>
     do
       let (mkbetree_internal_t i i0 n n0) := node
       let (st0, content) ← betree_load_internal_node_fwd i st
@@ -890,14 +883,14 @@ def betree_node_apply_messages_back
               node_id_cnt content0 st0
           let (mkbetree_internal_t i1 i2 n1 n2) := node0
           let _ ← betree_store_internal_node_fwd i1 content1 st1
-          Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t i1
-            i2 n1 n2), node_id_cnt0)
+          Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1 n2),
+            node_id_cnt0)
       else
         do
           let _ ← betree_store_internal_node_fwd i content0 st0
-          Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t i
-            i0 n n0), node_id_cnt)
-  | betree_node_t.BetreeNodeLeaf node =>
+          Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n n0),
+            node_id_cnt)
+  | betree_node_t.Leaf node =>
     do
       let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st
       let content0 ← betree_node_apply_messages_to_leaf_fwd_back content msgs
@@ -910,16 +903,16 @@ def betree_node_apply_messages_back
           let (st1, new_node) ←
             betree_leaf_split_fwd node content0 params node_id_cnt st0
           let _ ←
-            betree_store_leaf_node_fwd node.betree_leaf_id
-              betree_list_t.BetreeListNil st1
+            betree_store_leaf_node_fwd node.betree_leaf_id betree_list_t.Nil
+              st1
           let node_id_cnt0 ←
             betree_leaf_split_back node content0 params node_id_cnt st0
-          Result.ret (betree_node_t.BetreeNodeInternal new_node, node_id_cnt0)
+          Result.ret (betree_node_t.Internal new_node, node_id_cnt0)
       else
         do
           let _ ← betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
-          Result.ret (betree_node_t.BetreeNodeLeaf
-            { node with betree_leaf_size := len }, node_id_cnt)
+          Result.ret (betree_node_t.Leaf { node with betree_leaf_size := len },
+            node_id_cnt)
 termination_by betree_node_apply_messages_back self params node_id_cnt msgs st
   =>
   betree_node_apply_messages_terminates self params node_id_cnt msgs st
@@ -956,7 +949,7 @@ def betree_internal_flush_fwd
             let _ ←
               betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
                 st0
-            Result.ret (st1, betree_list_t.BetreeListNil)
+            Result.ret (st1, betree_list_t.Nil)
         else Result.ret (st0, msgs_right)
     else
       do
@@ -1017,13 +1010,13 @@ def betree_node_apply_fwd
   Result (State × Unit)
   :=
   do
-    let l := betree_list_t.BetreeListNil
+    let l := betree_list_t.Nil
     let (st0, _) ←
       betree_node_apply_messages_fwd self params node_id_cnt
-        (betree_list_t.BetreeListCons (key, new_msg) l) st
+        (betree_list_t.Cons (key, new_msg) l) st
     let _ ←
       betree_node_apply_messages_back self params node_id_cnt
-        (betree_list_t.BetreeListCons (key, new_msg) l) st
+        (betree_list_t.Cons (key, new_msg) l) st
     Result.ret (st0, ())
 
 /- [betree_main::betree::Node::{5}::apply] -/
@@ -1033,9 +1026,9 @@ def betree_node_apply_back
   (new_msg : betree_message_t) (st : State) :
   Result (betree_node_t × betree_node_id_counter_t)
   :=
-  let l := betree_list_t.BetreeListNil
-  betree_node_apply_messages_back self params node_id_cnt
-    (betree_list_t.BetreeListCons (key, new_msg) l) st
+  let l := betree_list_t.Nil
+  betree_node_apply_messages_back self params node_id_cnt (betree_list_t.Cons
+    (key, new_msg) l) st
 
 /- [betree_main::betree::BeTree::{6}::new] -/
 def betree_be_tree_new_fwd
@@ -1045,8 +1038,7 @@ def betree_be_tree_new_fwd
   do
     let node_id_cnt ← betree_node_id_counter_new_fwd
     let id ← betree_node_id_counter_fresh_id_fwd node_id_cnt
-    let (st0, _) ←
-      betree_store_leaf_node_fwd id betree_list_t.BetreeListNil st
+    let (st0, _) ← betree_store_leaf_node_fwd id betree_list_t.Nil st
     let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt
     Result.ret (st0,
       {
@@ -1057,7 +1049,7 @@ def betree_be_tree_new_fwd
           },
         betree_be_tree_node_id_cnt := node_id_cnt0,
         betree_be_tree_root :=
-          (betree_node_t.BetreeNodeLeaf
+          (betree_node_t.Leaf
             {
               betree_leaf_id := id,
               betree_leaf_size := (UInt64.ofNatCore 0 (by intlit))
@@ -1099,11 +1091,9 @@ def betree_be_tree_insert_fwd
   :=
   do
     let (st0, _) ←
-      betree_be_tree_apply_fwd self key (betree_message_t.BetreeMessageInsert
-        value) st
+      betree_be_tree_apply_fwd self key (betree_message_t.Insert value) st
     let _ ←
-      betree_be_tree_apply_back self key (betree_message_t.BetreeMessageInsert
-        value) st
+      betree_be_tree_apply_back self key (betree_message_t.Insert value) st
     Result.ret (st0, ())
 
 /- [betree_main::betree::BeTree::{6}::insert] -/
@@ -1111,8 +1101,7 @@ def betree_be_tree_insert_back
   (self : betree_be_tree_t) (key : UInt64) (value : UInt64) (st : State) :
   Result betree_be_tree_t
   :=
-  betree_be_tree_apply_back self key (betree_message_t.BetreeMessageInsert
-    value) st
+  betree_be_tree_apply_back self key (betree_message_t.Insert value) st
 
 /- [betree_main::betree::BeTree::{6}::delete] -/
 def betree_be_tree_delete_fwd
@@ -1121,10 +1110,8 @@ def betree_be_tree_delete_fwd
   :=
   do
     let (st0, _) ←
-      betree_be_tree_apply_fwd self key betree_message_t.BetreeMessageDelete st
-    let _ ←
-      betree_be_tree_apply_back self key betree_message_t.BetreeMessageDelete
-        st
+      betree_be_tree_apply_fwd self key betree_message_t.Delete st
+    let _ ← betree_be_tree_apply_back self key betree_message_t.Delete st
     Result.ret (st0, ())
 
 /- [betree_main::betree::BeTree::{6}::delete] -/
@@ -1132,7 +1119,7 @@ def betree_be_tree_delete_back
   (self : betree_be_tree_t) (key : UInt64) (st : State) :
   Result betree_be_tree_t
   :=
-  betree_be_tree_apply_back self key betree_message_t.BetreeMessageDelete st
+  betree_be_tree_apply_back self key betree_message_t.Delete st
 
 /- [betree_main::betree::BeTree::{6}::upsert] -/
 def betree_be_tree_upsert_fwd
@@ -1142,11 +1129,9 @@ def betree_be_tree_upsert_fwd
   :=
   do
     let (st0, _) ←
-      betree_be_tree_apply_fwd self key (betree_message_t.BetreeMessageUpsert
-        upd) st
+      betree_be_tree_apply_fwd self key (betree_message_t.Upsert upd) st
     let _ ←
-      betree_be_tree_apply_back self key (betree_message_t.BetreeMessageUpsert
-        upd) st
+      betree_be_tree_apply_back self key (betree_message_t.Upsert upd) st
     Result.ret (st0, ())
 
 /- [betree_main::betree::BeTree::{6}::upsert] -/
@@ -1155,8 +1140,7 @@ def betree_be_tree_upsert_back
   (st : State) :
   Result betree_be_tree_t
   :=
-  betree_be_tree_apply_back self key (betree_message_t.BetreeMessageUpsert upd)
-    st
+  betree_be_tree_apply_back self key (betree_message_t.Upsert upd) st
 
 /- [betree_main::betree::BeTree::{6}::lookup] -/
 def betree_be_tree_lookup_fwd
diff --git a/tests/lean/betree/BetreeMain/Types.lean b/tests/lean/betree/BetreeMain/Types.lean
index e2e6c867..32634e30 100644
--- a/tests/lean/betree/BetreeMain/Types.lean
+++ b/tests/lean/betree/BetreeMain/Types.lean
@@ -4,19 +4,19 @@ import Base.Primitives
 
 /- [betree_main::betree::List] -/
 inductive betree_list_t (T : Type) :=
-| BetreeListCons : T -> betree_list_t T -> betree_list_t T
-| BetreeListNil : betree_list_t T
+| Cons : T -> betree_list_t T -> betree_list_t T
+| Nil : betree_list_t T
 
 /- [betree_main::betree::UpsertFunState] -/
 inductive betree_upsert_fun_state_t :=
-| BetreeUpsertFunStateAdd : UInt64 -> betree_upsert_fun_state_t
-| BetreeUpsertFunStateSub : UInt64 -> betree_upsert_fun_state_t
+| Add : UInt64 -> betree_upsert_fun_state_t
+| Sub : UInt64 -> betree_upsert_fun_state_t
 
 /- [betree_main::betree::Message] -/
 inductive betree_message_t :=
-| BetreeMessageInsert : UInt64 -> betree_message_t
-| BetreeMessageDelete : betree_message_t
-| BetreeMessageUpsert : betree_upsert_fun_state_t -> betree_message_t
+| Insert : UInt64 -> betree_message_t
+| Delete : betree_message_t
+| Upsert : betree_upsert_fun_state_t -> betree_message_t
 
 /- [betree_main::betree::Leaf] -/
 structure betree_leaf_t where
@@ -25,8 +25,8 @@ structure betree_leaf_t where
 
 /- [betree_main::betree::Node] -/
 mutual inductive betree_node_t :=
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+| Internal : betree_internal_t -> betree_node_t
+| Leaf : betree_leaf_t -> betree_node_t
 
 /- [betree_main::betree::Internal] -/
 inductive betree_internal_t :=
diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean
index 0d83b04d..535ac9b2 100644
--- a/tests/lean/hashmap/Hashmap/Funs.lean
+++ b/tests/lean/hashmap/Hashmap/Funs.lean
@@ -16,7 +16,7 @@ def hash_map_allocate_slots_loop_fwd
   if h: n > (USize.ofNatCore 0 (by intlit))
   then
     do
-      let slots0 ← vec_push_back (list_t T) slots list_t.ListNil
+      let slots0 ← vec_push_back (list_t T) slots list_t.Nil
       let n0 ← USize.checked_sub n (USize.ofNatCore 1 (by intlit))
       hash_map_allocate_slots_loop_fwd T slots0 n0
   else Result.ret slots
@@ -63,7 +63,7 @@ def hash_map_clear_loop_fwd_back
   then
     do
       let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit))
-      let slots0 ← vec_index_mut_back (list_t T) slots i list_t.ListNil
+      let slots0 ← vec_index_mut_back (list_t T) slots i list_t.Nil
       hash_map_clear_loop_fwd_back T slots0 i1
   else Result.ret slots
 termination_by hash_map_clear_loop_fwd_back slots i =>
@@ -93,11 +93,11 @@ def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result USize :=
 def hash_map_insert_in_list_loop_fwd
   (T : Type) (key : USize) (value : T) (ls : list_t T) : (Result Bool) :=
   match h: ls with
-  | list_t.ListCons ckey cvalue tl =>
+  | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
     then Result.ret false
     else hash_map_insert_in_list_loop_fwd T key value tl
-  | list_t.ListNil => Result.ret true
+  | list_t.Nil => Result.ret true
 termination_by hash_map_insert_in_list_loop_fwd key value ls =>
   hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hash_map_insert_in_list_loop_decreases key value ls
@@ -111,16 +111,15 @@ def hash_map_insert_in_list_fwd
 def hash_map_insert_in_list_loop_back
   (T : Type) (key : USize) (value : T) (ls : list_t T) : (Result (list_t T)) :=
   match h: ls with
-  | list_t.ListCons ckey cvalue tl =>
+  | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
-    then Result.ret (list_t.ListCons ckey value tl)
+    then Result.ret (list_t.Cons ckey value tl)
     else
       do
         let tl0 ← hash_map_insert_in_list_loop_back T key value tl
-        Result.ret (list_t.ListCons ckey cvalue tl0)
-  | list_t.ListNil =>
-    let l := list_t.ListNil
-    Result.ret (list_t.ListCons key value l)
+        Result.ret (list_t.Cons ckey cvalue tl0)
+  | list_t.Nil => let l := list_t.Nil
+                  Result.ret (list_t.Cons key value l)
 termination_by hash_map_insert_in_list_loop_back key value ls =>
   hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hash_map_insert_in_list_loop_decreases key value ls
@@ -167,11 +166,11 @@ def hash_map_move_elements_from_list_loop_fwd_back
   (Result (hash_map_t T))
   :=
   match h: ls with
-  | list_t.ListCons k v tl =>
+  | list_t.Cons k v tl =>
     do
       let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v
       hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl
-  | list_t.ListNil => Result.ret ntable
+  | list_t.Nil => Result.ret ntable
 termination_by hash_map_move_elements_from_list_loop_fwd_back ntable ls =>
   hash_map_move_elements_from_list_loop_terminates T ntable ls
 decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls
@@ -191,10 +190,10 @@ def hash_map_move_elements_loop_fwd_back
   then
     do
       let l ← vec_index_mut_fwd (list_t T) slots i
-      let ls := mem_replace_fwd (list_t T) l list_t.ListNil
+      let ls := mem_replace_fwd (list_t T) l list_t.Nil
       let ntable0 ← hash_map_move_elements_from_list_fwd_back T ntable ls
       let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit))
-      let l0 := mem_replace_back (list_t T) l list_t.ListNil
+      let l0 := mem_replace_back (list_t T) l list_t.Nil
       let slots0 ← vec_index_mut_back (list_t T) slots i l0
       hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1
   else Result.ret (ntable, slots)
@@ -251,11 +250,11 @@ def hash_map_insert_fwd_back
 def hash_map_contains_key_in_list_loop_fwd
   (T : Type) (key : USize) (ls : list_t T) : (Result Bool) :=
   match h: ls with
-  | list_t.ListCons ckey t tl =>
+  | list_t.Cons ckey t tl =>
     if h: ckey = key
     then Result.ret true
     else hash_map_contains_key_in_list_loop_fwd T key tl
-  | list_t.ListNil => Result.ret false
+  | list_t.Nil => Result.ret false
 termination_by hash_map_contains_key_in_list_loop_fwd key ls =>
   hash_map_contains_key_in_list_loop_terminates T key ls
 decreasing_by hash_map_contains_key_in_list_loop_decreases key ls
@@ -279,11 +278,11 @@ def hash_map_contains_key_fwd
 def hash_map_get_in_list_loop_fwd
   (T : Type) (key : USize) (ls : list_t T) : (Result T) :=
   match h: ls with
-  | list_t.ListCons ckey cvalue tl =>
+  | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
     then Result.ret cvalue
     else hash_map_get_in_list_loop_fwd T key tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by hash_map_get_in_list_loop_fwd key ls =>
   hash_map_get_in_list_loop_terminates T key ls
 decreasing_by hash_map_get_in_list_loop_decreases key ls
@@ -307,11 +306,11 @@ def hash_map_get_fwd
 def hash_map_get_mut_in_list_loop_fwd
   (T : Type) (ls : list_t T) (key : USize) : (Result T) :=
   match h: ls with
-  | list_t.ListCons ckey cvalue tl =>
+  | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
     then Result.ret cvalue
     else hash_map_get_mut_in_list_loop_fwd T tl key
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by hash_map_get_mut_in_list_loop_fwd ls key =>
   hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
@@ -325,14 +324,14 @@ def hash_map_get_mut_in_list_fwd
 def hash_map_get_mut_in_list_loop_back
   (T : Type) (ls : list_t T) (key : USize) (ret0 : T) : (Result (list_t T)) :=
   match h: ls with
-  | list_t.ListCons ckey cvalue tl =>
+  | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
-    then Result.ret (list_t.ListCons ckey ret0 tl)
+    then Result.ret (list_t.Cons ckey ret0 tl)
     else
       do
         let tl0 ← hash_map_get_mut_in_list_loop_back T tl key ret0
-        Result.ret (list_t.ListCons ckey cvalue tl0)
-  | list_t.ListNil => Result.fail Error.panic
+        Result.ret (list_t.Cons ckey cvalue tl0)
+  | list_t.Nil => Result.fail Error.panic
 termination_by hash_map_get_mut_in_list_loop_back ls key ret0 =>
   hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
@@ -370,16 +369,16 @@ def hash_map_get_mut_back
 def hash_map_remove_from_list_loop_fwd
   (T : Type) (key : USize) (ls : list_t T) : (Result (Option T)) :=
   match h: ls with
-  | list_t.ListCons ckey t tl =>
+  | list_t.Cons ckey t tl =>
     if h: ckey = key
     then
       let mv_ls :=
-        mem_replace_fwd (list_t T) (list_t.ListCons ckey t tl) list_t.ListNil
+        mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil
       match h: mv_ls with
-      | list_t.ListCons i cvalue tl0 => Result.ret (Option.some cvalue)
-      | list_t.ListNil => Result.fail Error.panic
+      | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue)
+      | list_t.Nil => Result.fail Error.panic
     else hash_map_remove_from_list_loop_fwd T key tl
-  | list_t.ListNil => Result.ret Option.none
+  | list_t.Nil => Result.ret Option.none
 termination_by hash_map_remove_from_list_loop_fwd key ls =>
   hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hash_map_remove_from_list_loop_decreases key ls
@@ -393,19 +392,19 @@ def hash_map_remove_from_list_fwd
 def hash_map_remove_from_list_loop_back
   (T : Type) (key : USize) (ls : list_t T) : (Result (list_t T)) :=
   match h: ls with
-  | list_t.ListCons ckey t tl =>
+  | list_t.Cons ckey t tl =>
     if h: ckey = key
     then
       let mv_ls :=
-        mem_replace_fwd (list_t T) (list_t.ListCons ckey t tl) list_t.ListNil
+        mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil
       match h: mv_ls with
-      | list_t.ListCons i cvalue tl0 => Result.ret tl0
-      | list_t.ListNil => Result.fail Error.panic
+      | list_t.Cons i cvalue tl0 => Result.ret tl0
+      | list_t.Nil => Result.fail Error.panic
     else
       do
         let tl0 ← hash_map_remove_from_list_loop_back T key tl
-        Result.ret (list_t.ListCons ckey t tl0)
-  | list_t.ListNil => Result.ret list_t.ListNil
+        Result.ret (list_t.Cons ckey t tl0)
+  | list_t.Nil => Result.ret list_t.Nil
 termination_by hash_map_remove_from_list_loop_back key ls =>
   hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hash_map_remove_from_list_loop_decreases key ls
diff --git a/tests/lean/hashmap/Hashmap/Types.lean b/tests/lean/hashmap/Hashmap/Types.lean
index dd2be633..9e9e5c03 100644
--- a/tests/lean/hashmap/Hashmap/Types.lean
+++ b/tests/lean/hashmap/Hashmap/Types.lean
@@ -4,8 +4,8 @@ import Base.Primitives
 
 /- [hashmap::List] -/
 inductive list_t (T : Type) :=
-| ListCons : USize -> T -> list_t T -> list_t T
-| ListNil : list_t T
+| Cons : USize -> T -> list_t T -> list_t T
+| Nil : list_t T
 
 /- [hashmap::HashMap] -/
 structure hash_map_t (T : Type) where
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index bf3a30e9..2be03d98 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -19,8 +19,7 @@ def hashmap_hash_map_allocate_slots_loop_fwd
   if h: n > (USize.ofNatCore 0 (by intlit))
   then
     do
-      let slots0 ←
-        vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil
+      let slots0 ← vec_push_back (hashmap_list_t T) slots hashmap_list_t.Nil
       let n0 ← USize.checked_sub n (USize.ofNatCore 1 (by intlit))
       hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0
   else Result.ret slots
@@ -60,8 +59,8 @@ def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) :=
   hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit))
     (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit))
 
-/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
-def hashmap_hash_map_clear_slots_loop_fwd_back
+/- [hashmap_main::hashmap::HashMap::{0}::clear] -/
+def hashmap_hash_map_clear_loop_fwd_back
   (T : Type) (slots : Vec (hashmap_list_t T)) (i : USize) :
   (Result (Vec (hashmap_list_t T)))
   :=
@@ -71,28 +70,20 @@ def hashmap_hash_map_clear_slots_loop_fwd_back
     do
       let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit))
       let slots0 ←
-        vec_index_mut_back (hashmap_list_t T) slots i
-          hashmap_list_t.HashmapListNil
-      hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1
+        vec_index_mut_back (hashmap_list_t T) slots i hashmap_list_t.Nil
+      hashmap_hash_map_clear_loop_fwd_back T slots0 i1
   else Result.ret slots
-termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i =>
-  hashmap_hash_map_clear_slots_loop_terminates T slots i
-decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i
-
-/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
-def hashmap_hash_map_clear_slots_fwd_back
-  (T : Type) (slots : Vec (hashmap_list_t T)) :
-  Result (Vec (hashmap_list_t T))
-  :=
-  hashmap_hash_map_clear_slots_loop_fwd_back T slots
-    (USize.ofNatCore 0 (by intlit))
+termination_by hashmap_hash_map_clear_loop_fwd_back slots i =>
+  hashmap_hash_map_clear_loop_terminates T slots i
+decreasing_by hashmap_hash_map_clear_loop_decreases slots i
 
 /- [hashmap_main::hashmap::HashMap::{0}::clear] -/
 def hashmap_hash_map_clear_fwd_back
   (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) :=
   do
     let v ←
-      hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots
+      hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots
+        (USize.ofNatCore 0 (by intlit))
     Result.ret
       {
         self
@@ -112,11 +103,11 @@ def hashmap_hash_map_insert_in_list_loop_fwd
   (Result Bool)
   :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons ckey cvalue tl =>
+  | hashmap_list_t.Cons ckey cvalue tl =>
     if h: ckey = key
     then Result.ret false
     else hashmap_hash_map_insert_in_list_loop_fwd T key value tl
-  | hashmap_list_t.HashmapListNil => Result.ret true
+  | hashmap_list_t.Nil => Result.ret true
 termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls =>
   hashmap_hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls
@@ -132,16 +123,16 @@ def hashmap_hash_map_insert_in_list_loop_back
   (Result (hashmap_list_t T))
   :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons ckey cvalue tl =>
+  | hashmap_list_t.Cons ckey cvalue tl =>
     if h: ckey = key
-    then Result.ret (hashmap_list_t.HashmapListCons ckey value tl)
+    then Result.ret (hashmap_list_t.Cons ckey value tl)
     else
       do
         let tl0 ← hashmap_hash_map_insert_in_list_loop_back T key value tl
-        Result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0)
-  | hashmap_list_t.HashmapListNil =>
-    let l := hashmap_list_t.HashmapListNil
-    Result.ret (hashmap_list_t.HashmapListCons key value l)
+        Result.ret (hashmap_list_t.Cons ckey cvalue tl0)
+  | hashmap_list_t.Nil =>
+    let l := hashmap_list_t.Nil
+    Result.ret (hashmap_list_t.Cons key value l)
 termination_by hashmap_hash_map_insert_in_list_loop_back key value ls =>
   hashmap_hash_map_insert_in_list_loop_terminates T key value ls
 decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls
@@ -199,11 +190,11 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back
   (Result (hashmap_hash_map_t T))
   :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons k v tl =>
+  | hashmap_list_t.Cons k v tl =>
     do
       let ntable0 ← hashmap_hash_map_insert_no_resize_fwd_back T ntable k v
       hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl
-  | hashmap_list_t.HashmapListNil => Result.ret ntable
+  | hashmap_list_t.Nil => Result.ret ntable
 termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls
   =>
   hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls
@@ -227,13 +218,11 @@ def hashmap_hash_map_move_elements_loop_fwd_back
   then
     do
       let l ← vec_index_mut_fwd (hashmap_list_t T) slots i
-      let ls :=
-        mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.HashmapListNil
+      let ls := mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.Nil
       let ntable0 ←
         hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls
       let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit))
-      let l0 :=
-        mem_replace_back (hashmap_list_t T) l hashmap_list_t.HashmapListNil
+      let l0 := mem_replace_back (hashmap_list_t T) l hashmap_list_t.Nil
       let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i l0
       hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1
   else Result.ret (ntable, slots)
@@ -291,11 +280,11 @@ def hashmap_hash_map_insert_fwd_back
 def hashmap_hash_map_contains_key_in_list_loop_fwd
   (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result Bool) :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons ckey t tl =>
+  | hashmap_list_t.Cons ckey t tl =>
     if h: ckey = key
     then Result.ret true
     else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl
-  | hashmap_list_t.HashmapListNil => Result.ret false
+  | hashmap_list_t.Nil => Result.ret false
 termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls =>
   hashmap_hash_map_contains_key_in_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls
@@ -320,11 +309,11 @@ def hashmap_hash_map_contains_key_fwd
 def hashmap_hash_map_get_in_list_loop_fwd
   (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result T) :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons ckey cvalue tl =>
+  | hashmap_list_t.Cons ckey cvalue tl =>
     if h: ckey = key
     then Result.ret cvalue
     else hashmap_hash_map_get_in_list_loop_fwd T key tl
-  | hashmap_list_t.HashmapListNil => Result.fail Error.panic
+  | hashmap_list_t.Nil => Result.fail Error.panic
 termination_by hashmap_hash_map_get_in_list_loop_fwd key ls =>
   hashmap_hash_map_get_in_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls
@@ -349,11 +338,11 @@ def hashmap_hash_map_get_fwd
 def hashmap_hash_map_get_mut_in_list_loop_fwd
   (T : Type) (ls : hashmap_list_t T) (key : USize) : (Result T) :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons ckey cvalue tl =>
+  | hashmap_list_t.Cons ckey cvalue tl =>
     if h: ckey = key
     then Result.ret cvalue
     else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key
-  | hashmap_list_t.HashmapListNil => Result.fail Error.panic
+  | hashmap_list_t.Nil => Result.fail Error.panic
 termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key =>
   hashmap_hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key
@@ -369,14 +358,14 @@ def hashmap_hash_map_get_mut_in_list_loop_back
   (Result (hashmap_list_t T))
   :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons ckey cvalue tl =>
+  | hashmap_list_t.Cons ckey cvalue tl =>
     if h: ckey = key
-    then Result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl)
+    then Result.ret (hashmap_list_t.Cons ckey ret0 tl)
     else
       do
         let tl0 ← hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0
-        Result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0)
-  | hashmap_list_t.HashmapListNil => Result.fail Error.panic
+        Result.ret (hashmap_list_t.Cons ckey cvalue tl0)
+  | hashmap_list_t.Nil => Result.fail Error.panic
 termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 =>
   hashmap_hash_map_get_mut_in_list_loop_terminates T ls key
 decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key
@@ -420,18 +409,17 @@ def hashmap_hash_map_get_mut_back
 def hashmap_hash_map_remove_from_list_loop_fwd
   (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result (Option T)) :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons ckey t tl =>
+  | hashmap_list_t.Cons ckey t tl =>
     if h: ckey = key
     then
       let mv_ls :=
-        mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey
-          t tl) hashmap_list_t.HashmapListNil
+        mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl)
+          hashmap_list_t.Nil
       match h: mv_ls with
-      | hashmap_list_t.HashmapListCons i cvalue tl0 =>
-        Result.ret (Option.some cvalue)
-      | hashmap_list_t.HashmapListNil => Result.fail Error.panic
+      | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue)
+      | hashmap_list_t.Nil => Result.fail Error.panic
     else hashmap_hash_map_remove_from_list_loop_fwd T key tl
-  | hashmap_list_t.HashmapListNil => Result.ret Option.none
+  | hashmap_list_t.Nil => Result.ret Option.none
 termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls =>
   hashmap_hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls
@@ -447,20 +435,20 @@ def hashmap_hash_map_remove_from_list_loop_back
   (Result (hashmap_list_t T))
   :=
   match h: ls with
-  | hashmap_list_t.HashmapListCons ckey t tl =>
+  | hashmap_list_t.Cons ckey t tl =>
     if h: ckey = key
     then
       let mv_ls :=
-        mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey
-          t tl) hashmap_list_t.HashmapListNil
+        mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl)
+          hashmap_list_t.Nil
       match h: mv_ls with
-      | hashmap_list_t.HashmapListCons i cvalue tl0 => Result.ret tl0
-      | hashmap_list_t.HashmapListNil => Result.fail Error.panic
+      | hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0
+      | hashmap_list_t.Nil => Result.fail Error.panic
     else
       do
         let tl0 ← hashmap_hash_map_remove_from_list_loop_back T key tl
-        Result.ret (hashmap_list_t.HashmapListCons ckey t tl0)
-  | hashmap_list_t.HashmapListNil => Result.ret hashmap_list_t.HashmapListNil
+        Result.ret (hashmap_list_t.Cons ckey t tl0)
+  | hashmap_list_t.Nil => Result.ret hashmap_list_t.Nil
 termination_by hashmap_hash_map_remove_from_list_loop_back key ls =>
   hashmap_hash_map_remove_from_list_loop_terminates T key ls
 decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
index fbab1bcd..989dd2a9 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
@@ -4,8 +4,8 @@ import Base.Primitives
 
 /- [hashmap_main::hashmap::List] -/
 inductive hashmap_list_t (T : Type) :=
-| HashmapListCons : USize -> T -> hashmap_list_t T -> hashmap_list_t T
-| HashmapListNil : hashmap_list_t T
+| Cons : USize -> T -> hashmap_list_t T -> hashmap_list_t T
+| Nil : hashmap_list_t T
 
 /- [hashmap_main::hashmap::HashMap] -/
 structure hashmap_hash_map_t (T : Type) where
diff --git a/tests/lean/misc-loops/Loops/Funs.lean b/tests/lean/misc-loops/Loops/Funs.lean
index 5a81ebff..f79a27a9 100644
--- a/tests/lean/misc-loops/Loops/Funs.lean
+++ b/tests/lean/misc-loops/Loops/Funs.lean
@@ -79,11 +79,11 @@ def clear_fwd_back (v : Vec UInt32) : Result (Vec UInt32) :=
 /- [loops::list_mem] -/
 def list_mem_loop_fwd (x : UInt32) (ls : list_t UInt32) : (Result Bool) :=
   match h: ls with
-  | list_t.ListCons y tl =>
+  | list_t.Cons y tl =>
     if h: y = x
     then Result.ret true
     else list_mem_loop_fwd x tl
-  | list_t.ListNil => Result.ret false
+  | list_t.Nil => Result.ret false
 termination_by list_mem_loop_fwd x ls => list_mem_loop_terminates x ls
 decreasing_by list_mem_loop_decreases x ls
 
@@ -95,14 +95,14 @@ def list_mem_fwd (x : UInt32) (ls : list_t UInt32) : Result Bool :=
 def list_nth_mut_loop_loop_fwd
   (T : Type) (ls : list_t T) (i : UInt32) : (Result T) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_mut_loop_loop_fwd T tl i0
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_loop_fwd ls i =>
   list_nth_mut_loop_loop_terminates T ls i
 decreasing_by list_nth_mut_loop_loop_decreases ls i
@@ -115,15 +115,15 @@ def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : UInt32) : Result T :=
 def list_nth_mut_loop_loop_back
   (T : Type) (ls : list_t T) (i : UInt32) (ret0 : T) : (Result (list_t T)) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
-    then Result.ret (list_t.ListCons ret0 tl)
+    then Result.ret (list_t.Cons ret0 tl)
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
-        Result.ret (list_t.ListCons x tl0)
-  | list_t.ListNil => Result.fail Error.panic
+        Result.ret (list_t.Cons x tl0)
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_loop_back ls i ret0 =>
   list_nth_mut_loop_loop_terminates T ls i
 decreasing_by list_nth_mut_loop_loop_decreases ls i
@@ -137,14 +137,14 @@ def list_nth_mut_loop_back
 def list_nth_shared_loop_loop_fwd
   (T : Type) (ls : list_t T) (i : UInt32) : (Result T) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_shared_loop_loop_fwd T tl i0
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_loop_loop_fwd ls i =>
   list_nth_shared_loop_loop_terminates T ls i
 decreasing_by list_nth_shared_loop_loop_decreases ls i
@@ -157,11 +157,11 @@ def list_nth_shared_loop_fwd
 /- [loops::get_elem_mut] -/
 def get_elem_mut_loop_fwd (x : USize) (ls : list_t USize) : (Result USize) :=
   match h: ls with
-  | list_t.ListCons y tl =>
+  | list_t.Cons y tl =>
     if h: y = x
     then Result.ret y
     else get_elem_mut_loop_fwd x tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by get_elem_mut_loop_fwd x ls => get_elem_mut_loop_terminates x ls
 decreasing_by get_elem_mut_loop_decreases x ls
 
@@ -176,14 +176,14 @@ def get_elem_mut_fwd (slots : Vec (list_t USize)) (x : USize) : Result USize :=
 def get_elem_mut_loop_back
   (x : USize) (ls : list_t USize) (ret0 : USize) : (Result (list_t USize)) :=
   match h: ls with
-  | list_t.ListCons y tl =>
+  | list_t.Cons y tl =>
     if h: y = x
-    then Result.ret (list_t.ListCons ret0 tl)
+    then Result.ret (list_t.Cons ret0 tl)
     else
       do
         let tl0 ← get_elem_mut_loop_back x tl ret0
-        Result.ret (list_t.ListCons y tl0)
-  | list_t.ListNil => Result.fail Error.panic
+        Result.ret (list_t.Cons y tl0)
+  | list_t.Nil => Result.fail Error.panic
 termination_by get_elem_mut_loop_back x ls ret0 =>
   get_elem_mut_loop_terminates x ls
 decreasing_by get_elem_mut_loop_decreases x ls
@@ -203,11 +203,11 @@ def get_elem_mut_back
 def get_elem_shared_loop_fwd
   (x : USize) (ls : list_t USize) : (Result USize) :=
   match h: ls with
-  | list_t.ListCons y tl =>
+  | list_t.Cons y tl =>
     if h: y = x
     then Result.ret y
     else get_elem_shared_loop_fwd x tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by get_elem_shared_loop_fwd x ls =>
   get_elem_shared_loop_terminates x ls
 decreasing_by get_elem_shared_loop_decreases x ls
@@ -237,14 +237,14 @@ def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
 def list_nth_mut_loop_with_id_loop_fwd
   (T : Type) (i : UInt32) (ls : list_t T) : (Result T) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_mut_loop_with_id_loop_fwd T i0 tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_with_id_loop_fwd i ls =>
   list_nth_mut_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls
@@ -260,15 +260,15 @@ def list_nth_mut_loop_with_id_fwd
 def list_nth_mut_loop_with_id_loop_back
   (T : Type) (i : UInt32) (ls : list_t T) (ret0 : T) : (Result (list_t T)) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
-    then Result.ret (list_t.ListCons ret0 tl)
+    then Result.ret (list_t.Cons ret0 tl)
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
-        Result.ret (list_t.ListCons x tl0)
-  | list_t.ListNil => Result.fail Error.panic
+        Result.ret (list_t.Cons x tl0)
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_with_id_loop_back i ls ret0 =>
   list_nth_mut_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls
@@ -285,14 +285,14 @@ def list_nth_mut_loop_with_id_back
 def list_nth_shared_loop_with_id_loop_fwd
   (T : Type) (i : UInt32) (ls : list_t T) : (Result T) :=
   match h: ls with
-  | list_t.ListCons x tl =>
+  | list_t.Cons x tl =>
     if h: i = (UInt32.ofNatCore 0 (by intlit))
     then Result.ret x
     else
       do
         let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
         list_nth_shared_loop_with_id_loop_fwd T i0 tl
-  | list_t.ListNil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_loop_with_id_loop_fwd i ls =>
   list_nth_shared_loop_with_id_loop_terminates T i ls
 decreasing_by list_nth_shared_loop_with_id_loop_decreases i ls
@@ -310,17 +310,17 @@ def list_nth_mut_loop_pair_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -338,18 +338,18 @@ def list_nth_mut_loop_pair_loop_back'a
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl0)
+      then Result.ret (list_t.Cons ret0 tl0)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x0 tl00)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -367,18 +367,18 @@ def list_nth_mut_loop_pair_loop_back'b
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl1)
+      then Result.ret (list_t.Cons ret0 tl1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x1 tl10)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -396,17 +396,17 @@ def list_nth_shared_loop_pair_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -424,17 +424,17 @@ def list_nth_mut_loop_pair_merge_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -452,21 +452,21 @@ def list_nth_mut_loop_pair_merge_loop_back
   (Result ((list_t T) × (list_t T)))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then
         let (t, t0) := ret0
-        Result.ret (list_t.ListCons t tl0, list_t.ListCons t0 tl1)
+        Result.ret (list_t.Cons t tl0, list_t.Cons t0 tl1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let (tl00, tl10) ←
             list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x0 tl00, list_t.ListCons x1 tl10)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x0 tl00, list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -484,17 +484,17 @@ def list_nth_shared_loop_pair_merge_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -512,17 +512,17 @@ def list_nth_mut_shared_loop_pair_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -540,19 +540,19 @@ def list_nth_mut_shared_loop_pair_loop_back
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl0)
+      then Result.ret (list_t.Cons ret0 tl0)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl00 ←
             list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x0 tl00)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i
@@ -570,17 +570,17 @@ def list_nth_mut_shared_loop_pair_merge_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -598,19 +598,19 @@ def list_nth_mut_shared_loop_pair_merge_loop_back
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl0)
+      then Result.ret (list_t.Cons ret0 tl0)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl00 ←
             list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x0 tl00)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x0 tl00)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -628,17 +628,17 @@ def list_nth_shared_mut_loop_pair_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i =>
   list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -656,19 +656,19 @@ def list_nth_shared_mut_loop_pair_loop_back
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl1)
+      then Result.ret (list_t.Cons ret0 tl1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl10 ←
             list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x1 tl10)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret0 =>
   list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i
@@ -686,17 +686,17 @@ def list_nth_shared_mut_loop_pair_merge_loop_fwd
   (Result (T × T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret (x0, x1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i =>
   list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i
@@ -714,19 +714,19 @@ def list_nth_shared_mut_loop_pair_merge_loop_back
   (Result (list_t T))
   :=
   match h: ls0 with
-  | list_t.ListCons x0 tl0 =>
+  | list_t.Cons x0 tl0 =>
     match h: ls1 with
-    | list_t.ListCons x1 tl1 =>
+    | list_t.Cons x1 tl1 =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl1)
+      then Result.ret (list_t.Cons ret0 tl1)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl10 ←
             list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
-          Result.ret (list_t.ListCons x1 tl10)
-    | list_t.ListNil => Result.fail Error.panic
-  | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x1 tl10)
+    | list_t.Nil => Result.fail Error.panic
+  | list_t.Nil => Result.fail Error.panic
 termination_by list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 =>
   list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i
 decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i
diff --git a/tests/lean/misc-loops/Loops/Types.lean b/tests/lean/misc-loops/Loops/Types.lean
index f4b6809e..ca43f4c8 100644
--- a/tests/lean/misc-loops/Loops/Types.lean
+++ b/tests/lean/misc-loops/Loops/Types.lean
@@ -4,6 +4,6 @@ import Base.Primitives
 
 /- [loops::List] -/
 inductive list_t (T : Type) :=
-| ListCons : T -> list_t T -> list_t T
-| ListNil : list_t T
+| Cons : T -> list_t T -> list_t T
+| Nil : list_t T
 
diff --git a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
index 12d4190c..e2697385 100644
--- a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
+++ b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean
@@ -11,29 +11,29 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::List] -/
   inductive list_t (T : Type) :=
-  | ListCons : T -> list_t T -> list_t T
-  | ListNil : list_t T
+  | Cons : T -> list_t T -> list_t T
+  | Nil : list_t T
   
   /- [no_nested_borrows::One] -/
   inductive one_t (T1 : Type) :=
-  | OneOne : T1 -> one_t T1
+  | One : T1 -> one_t T1
   
   /- [no_nested_borrows::EmptyEnum] -/
   inductive empty_enum_t :=
-  | EmptyEnumEmpty : empty_enum_t
+  | Empty : empty_enum_t
   
   /- [no_nested_borrows::Enum] -/
   inductive enum_t :=
-  | EnumVariant1 : enum_t
-  | EnumVariant2 : enum_t
+  | Variant1 : enum_t
+  | Variant2 : enum_t
   
   /- [no_nested_borrows::EmptyStruct] -/
   structure empty_struct_t where
   
   /- [no_nested_borrows::Sum] -/
   inductive sum_t (T1 T2 : Type) :=
-  | SumLeft : T1 -> sum_t T1 T2
-  | SumRight : T2 -> sum_t T1 T2
+  | Left : T1 -> sum_t T1 T2
+  | Right : T2 -> sum_t T1 T2
   
   /- [no_nested_borrows::neg_test] -/
   def neg_test_fwd (x : Int32) : Result Int32 :=
@@ -187,15 +187,15 @@ structure OpaqueDefs where
   /- [no_nested_borrows::is_cons] -/
   def is_cons_fwd (T : Type) (l : list_t T) : Result Bool :=
     match h: l with
-    | list_t.ListCons t l0 => Result.ret true
-    | list_t.ListNil => Result.ret false
+    | list_t.Cons t l0 => Result.ret true
+    | list_t.Nil => Result.ret false
   
   /- [no_nested_borrows::test_is_cons] -/
   def test_is_cons_fwd : Result Unit :=
     do
-      let l := list_t.ListNil
+      let l := list_t.Nil
       let b ←
-        is_cons_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit)) l)
+        is_cons_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l)
       if h: not b
       then Result.fail Error.panic
       else Result.ret ()
@@ -206,16 +206,15 @@ structure OpaqueDefs where
   /- [no_nested_borrows::split_list] -/
   def split_list_fwd (T : Type) (l : list_t T) : Result (T × (list_t T)) :=
     match h: l with
-    | list_t.ListCons hd tl => Result.ret (hd, tl)
-    | list_t.ListNil => Result.fail Error.panic
+    | list_t.Cons hd tl => Result.ret (hd, tl)
+    | list_t.Nil => Result.fail Error.panic
   
   /- [no_nested_borrows::test_split_list] -/
   def test_split_list_fwd : Result Unit :=
     do
-      let l := list_t.ListNil
+      let l := list_t.Nil
       let p ←
-        split_list_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit))
-          l)
+        split_list_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l)
       let (hd, _) := p
       if h: not (hd = (Int32.ofNatCore 0 (by intlit)))
       then Result.fail Error.panic
@@ -267,88 +266,87 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::NodeElem] -/
   mutual inductive node_elem_t (T : Type) :=
-  | NodeElemCons : tree_t T -> node_elem_t T -> node_elem_t T
-  | NodeElemNil : node_elem_t T
+  | Cons : tree_t T -> node_elem_t T -> node_elem_t T
+  | Nil : node_elem_t T
   
   /- [no_nested_borrows::Tree] -/
   inductive tree_t (T : Type) :=
-  | TreeLeaf : T -> tree_t T
-  | TreeNode : T -> node_elem_t T -> tree_t T -> tree_t T
+  | Leaf : T -> tree_t T
+  | Node : T -> node_elem_t T -> tree_t T -> tree_t T
   
   /- [no_nested_borrows::list_length] -/
   def list_length_fwd (T : Type) (l : list_t T) : Result UInt32 :=
     match h: l with
-    | list_t.ListCons t l1 =>
+    | list_t.Cons t l1 =>
       do
         let i ← list_length_fwd T l1
         UInt32.checked_add (UInt32.ofNatCore 1 (by intlit)) i
-    | list_t.ListNil => Result.ret (UInt32.ofNatCore 0 (by intlit))
+    | list_t.Nil => Result.ret (UInt32.ofNatCore 0 (by intlit))
   
   /- [no_nested_borrows::list_nth_shared] -/
   def list_nth_shared_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret x
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_shared_fwd T tl i0
-    | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
   
   /- [no_nested_borrows::list_nth_mut] -/
   def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret x
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_fwd T tl i0
-    | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
   
   /- [no_nested_borrows::list_nth_mut] -/
   def list_nth_mut_back
     (T : Type) (l : list_t T) (i : UInt32) (ret0 : T) : Result (list_t T) :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl)
+      then Result.ret (list_t.Cons ret0 tl)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl0 ← list_nth_mut_back T tl i0 ret0
-          Result.ret (list_t.ListCons x tl0)
-    | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x tl0)
+    | list_t.Nil => Result.fail Error.panic
   
   /- [no_nested_borrows::list_rev_aux] -/
   def list_rev_aux_fwd
     (T : Type) (li : list_t T) (lo : list_t T) : Result (list_t T) :=
     match h: li with
-    | list_t.ListCons hd tl => list_rev_aux_fwd T tl (list_t.ListCons hd lo)
-    | list_t.ListNil => Result.ret lo
+    | list_t.Cons hd tl => list_rev_aux_fwd T tl (list_t.Cons hd lo)
+    | list_t.Nil => Result.ret lo
   
   /- [no_nested_borrows::list_rev] -/
   def list_rev_fwd_back (T : Type) (l : list_t T) : Result (list_t T) :=
-    let li := mem_replace_fwd (list_t T) l list_t.ListNil
-    list_rev_aux_fwd T li list_t.ListNil
+    let li := mem_replace_fwd (list_t T) l list_t.Nil
+    list_rev_aux_fwd T li list_t.Nil
   
   /- [no_nested_borrows::test_list_functions] -/
   def test_list_functions_fwd : Result Unit :=
     do
-      let l := list_t.ListNil
-      let l0 := list_t.ListCons (Int32.ofNatCore 2 (by intlit)) l
-      let l1 := list_t.ListCons (Int32.ofNatCore 1 (by intlit)) l0
+      let l := list_t.Nil
+      let l0 := list_t.Cons (Int32.ofNatCore 2 (by intlit)) l
+      let l1 := list_t.Cons (Int32.ofNatCore 1 (by intlit)) l0
       let i ←
-        list_length_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit))
-          l1)
+        list_length_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l1)
       if h: not (i = (UInt32.ofNatCore 3 (by intlit)))
       then Result.fail Error.panic
       else
         do
           let i0 ←
-            list_nth_shared_fwd Int32 (list_t.ListCons
+            list_nth_shared_fwd Int32 (list_t.Cons
               (Int32.ofNatCore 0 (by intlit)) l1)
               (UInt32.ofNatCore 0 (by intlit))
           if h: not (i0 = (Int32.ofNatCore 0 (by intlit)))
@@ -356,7 +354,7 @@ structure OpaqueDefs where
           else
             do
               let i1 ←
-                list_nth_shared_fwd Int32 (list_t.ListCons
+                list_nth_shared_fwd Int32 (list_t.Cons
                   (Int32.ofNatCore 0 (by intlit)) l1)
                   (UInt32.ofNatCore 1 (by intlit))
               if h: not (i1 = (Int32.ofNatCore 1 (by intlit)))
@@ -364,7 +362,7 @@ structure OpaqueDefs where
               else
                 do
                   let i2 ←
-                    list_nth_shared_fwd Int32 (list_t.ListCons
+                    list_nth_shared_fwd Int32 (list_t.Cons
                       (Int32.ofNatCore 0 (by intlit)) l1)
                       (UInt32.ofNatCore 2 (by intlit))
                   if h: not (i2 = (Int32.ofNatCore 2 (by intlit)))
@@ -372,7 +370,7 @@ structure OpaqueDefs where
                   else
                     do
                       let ls ←
-                        list_nth_mut_back Int32 (list_t.ListCons
+                        list_nth_mut_back Int32 (list_t.Cons
                           (Int32.ofNatCore 0 (by intlit)) l1)
                           (UInt32.ofNatCore 1 (by intlit))
                           (Int32.ofNatCore 3 (by intlit))
@@ -550,8 +548,8 @@ structure OpaqueDefs where
   /- [no_nested_borrows::test_shared_borrow_enum1] -/
   def test_shared_borrow_enum1_fwd (l : list_t UInt32) : Result UInt32 :=
     match h: l with
-    | list_t.ListCons i l0 => Result.ret (UInt32.ofNatCore 1 (by intlit))
-    | list_t.ListNil => Result.ret (UInt32.ofNatCore 0 (by intlit))
+    | list_t.Cons i l0 => Result.ret (UInt32.ofNatCore 1 (by intlit))
+    | list_t.Nil => Result.ret (UInt32.ofNatCore 0 (by intlit))
   
   /- [no_nested_borrows::test_shared_borrow_enum2] -/
   def test_shared_borrow_enum2_fwd : Result UInt32 :=
diff --git a/tests/lean/misc-paper/Paper.lean b/tests/lean/misc-paper/Paper.lean
index 4faf36ee..05fde52c 100644
--- a/tests/lean/misc-paper/Paper.lean
+++ b/tests/lean/misc-paper/Paper.lean
@@ -58,57 +58,56 @@ structure OpaqueDefs where
   
   /- [paper::List] -/
   inductive list_t (T : Type) :=
-  | ListCons : T -> list_t T -> list_t T
-  | ListNil : list_t T
+  | Cons : T -> list_t T -> list_t T
+  | Nil : list_t T
   
   /- [paper::list_nth_mut] -/
   def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
       then Result.ret x
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           list_nth_mut_fwd T tl i0
-    | list_t.ListNil => Result.fail Error.panic
+    | list_t.Nil => Result.fail Error.panic
   
   /- [paper::list_nth_mut] -/
   def list_nth_mut_back
     (T : Type) (l : list_t T) (i : UInt32) (ret0 : T) : Result (list_t T) :=
     match h: l with
-    | list_t.ListCons x tl =>
+    | list_t.Cons x tl =>
       if h: i = (UInt32.ofNatCore 0 (by intlit))
-      then Result.ret (list_t.ListCons ret0 tl)
+      then Result.ret (list_t.Cons ret0 tl)
       else
         do
           let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit))
           let tl0 ← list_nth_mut_back T tl i0 ret0
-          Result.ret (list_t.ListCons x tl0)
-    | list_t.ListNil => Result.fail Error.panic
+          Result.ret (list_t.Cons x tl0)
+    | list_t.Nil => Result.fail Error.panic
   
   /- [paper::sum] -/
   def sum_fwd (l : list_t Int32) : Result Int32 :=
     match h: l with
-    | list_t.ListCons x tl => do
-                                let i ← sum_fwd tl
-                                Int32.checked_add x i
-    | list_t.ListNil => Result.ret (Int32.ofNatCore 0 (by intlit))
+    | list_t.Cons x tl => do
+                            let i ← sum_fwd tl
+                            Int32.checked_add x i
+    | list_t.Nil => Result.ret (Int32.ofNatCore 0 (by intlit))
   
   /- [paper::test_nth] -/
   def test_nth_fwd : Result Unit :=
     do
-      let l := list_t.ListNil
-      let l0 := list_t.ListCons (Int32.ofNatCore 3 (by intlit)) l
-      let l1 := list_t.ListCons (Int32.ofNatCore 2 (by intlit)) l0
+      let l := list_t.Nil
+      let l0 := list_t.Cons (Int32.ofNatCore 3 (by intlit)) l
+      let l1 := list_t.Cons (Int32.ofNatCore 2 (by intlit)) l0
       let x ←
-        list_nth_mut_fwd Int32 (list_t.ListCons (Int32.ofNatCore 1 (by intlit))
-          l1) (UInt32.ofNatCore 2 (by intlit))
+        list_nth_mut_fwd Int32 (list_t.Cons (Int32.ofNatCore 1 (by intlit)) l1)
+          (UInt32.ofNatCore 2 (by intlit))
       let x0 ← Int32.checked_add x (Int32.ofNatCore 1 (by intlit))
       let l2 ←
-        list_nth_mut_back Int32 (list_t.ListCons
-          (Int32.ofNatCore 1 (by intlit)) l1) (UInt32.ofNatCore 2 (by intlit))
-          x0
+        list_nth_mut_back Int32 (list_t.Cons (Int32.ofNatCore 1 (by intlit))
+          l1) (UInt32.ofNatCore 2 (by intlit)) x0
       let i ← sum_fwd l2
       if h: not (i = (Int32.ofNatCore 7 (by intlit)))
       then Result.fail Error.panic
diff --git a/tests/lean/misc-polonius_list/PoloniusList.lean b/tests/lean/misc-polonius_list/PoloniusList.lean
index d679230d..a3bbfd0a 100644
--- a/tests/lean/misc-polonius_list/PoloniusList.lean
+++ b/tests/lean/misc-polonius_list/PoloniusList.lean
@@ -6,18 +6,18 @@ structure OpaqueDefs where
   
   /- [polonius_list::List] -/
   inductive list_t (T : Type) :=
-  | ListCons : T -> list_t T -> list_t T
-  | ListNil : list_t T
+  | Cons : T -> list_t T -> list_t T
+  | Nil : list_t T
   
   /- [polonius_list::get_list_at_x] -/
   def get_list_at_x_fwd
     (ls : list_t UInt32) (x : UInt32) : Result (list_t UInt32) :=
     match h: ls with
-    | list_t.ListCons hd tl =>
+    | list_t.Cons hd tl =>
       if h: hd = x
-      then Result.ret (list_t.ListCons hd tl)
+      then Result.ret (list_t.Cons hd tl)
       else get_list_at_x_fwd tl x
-    | list_t.ListNil => Result.ret list_t.ListNil
+    | list_t.Nil => Result.ret list_t.Nil
   
   /- [polonius_list::get_list_at_x] -/
   def get_list_at_x_back
@@ -25,12 +25,12 @@ structure OpaqueDefs where
     Result (list_t UInt32)
     :=
     match h: ls with
-    | list_t.ListCons hd tl =>
+    | list_t.Cons hd tl =>
       if h: hd = x
       then Result.ret ret0
       else
         do
           let tl0 ← get_list_at_x_back tl x ret0
-          Result.ret (list_t.ListCons hd tl0)
-    | list_t.ListNil => Result.ret ret0
+          Result.ret (list_t.Cons hd tl0)
+    | list_t.Nil => Result.ret ret0