Merge branch 'main' into unsigned-max

3 files changed, 2195 insertions, 0 deletions

diff --git a/tests/hol4/no_nested_borrows/Holmakefile b/tests/hol4/no_nested_borrows/Holmakefile
new file mode 100644
index 00000000..3c4b8973
--- /dev/null
+++ b/tests/hol4/no_nested_borrows/Holmakefile
@@ -0,0 +1,5 @@
+# This file was automatically generated - modify ../Holmakefile.template instead
+INCLUDES =  ../../../backends/hol4
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/tests/hol4/no_nested_borrows/noNestedBorrowsScript.sml b/tests/hol4/no_nested_borrows/noNestedBorrowsScript.sml
new file mode 100644
index 00000000..1b2d6121
--- /dev/null
+++ b/tests/hol4/no_nested_borrows/noNestedBorrowsScript.sml
@@ -0,0 +1,592 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [no_nested_borrows] *)
+open primitivesLib divDefLib
+
+val _ = new_theory "noNestedBorrows"
+
+
+Datatype:
+  (** [no_nested_borrows::Pair] *)
+  pair_t = <| pair_x : 't1; pair_y : 't2; |>
+End
+
+Datatype:
+  (** [no_nested_borrows::List] *)
+  list_t = | ListCons 't list_t | ListNil
+End
+
+Datatype:
+  (** [no_nested_borrows::One] *)
+  one_t = | OneOne 't1
+End
+
+Datatype:
+  (** [no_nested_borrows::EmptyEnum] *)
+  empty_enum_t = | EmptyEnumEmpty
+End
+
+Datatype:
+  (** [no_nested_borrows::Enum] *)
+  enum_t = | EnumVariant1 | EnumVariant2
+End
+
+Type empty_struct_t = “: unit”
+
+Datatype:
+  (** [no_nested_borrows::Sum] *)
+  sum_t = | SumLeft 't1 | SumRight 't2
+End
+
+val neg_test_fwd_def = Define ‘
+  (** [no_nested_borrows::neg_test]: forward function *)
+  neg_test_fwd (x : i32) : i32 result =
+    i32_neg x
+’
+
+val add_test_fwd_def = Define ‘
+  (** [no_nested_borrows::add_test]: forward function *)
+  add_test_fwd (x : u32) (y : u32) : u32 result =
+    u32_add x y
+’
+
+val subs_test_fwd_def = Define ‘
+  (** [no_nested_borrows::subs_test]: forward function *)
+  subs_test_fwd (x : u32) (y : u32) : u32 result =
+    u32_sub x y
+’
+
+val div_test_fwd_def = Define ‘
+  (** [no_nested_borrows::div_test]: forward function *)
+  div_test_fwd (x : u32) (y : u32) : u32 result =
+    u32_div x y
+’
+
+val div_test1_fwd_def = Define ‘
+  (** [no_nested_borrows::div_test1]: forward function *)
+  div_test1_fwd (x : u32) : u32 result =
+    u32_div x (int_to_u32 2)
+’
+
+val rem_test_fwd_def = Define ‘
+  (** [no_nested_borrows::rem_test]: forward function *)
+  rem_test_fwd (x : u32) (y : u32) : u32 result =
+    u32_rem x y
+’
+
+val cast_test_fwd_def = Define ‘
+  (** [no_nested_borrows::cast_test]: forward function *)
+  cast_test_fwd (x : u32) : i32 result =
+    mk_i32 (u32_to_int x)
+’
+
+val test2_fwd_def = Define ‘
+  (** [no_nested_borrows::test2]: forward function *)
+  test2_fwd : unit result =
+    do
+    _ <- u32_add (int_to_u32 23) (int_to_u32 44);
+    Return ()
+    od
+’
+
+(** Unit test for [no_nested_borrows::test2] *)
+val _ = assert_return (“test2_fwd”)
+
+val get_max_fwd_def = Define ‘
+  (** [no_nested_borrows::get_max]: forward function *)
+  get_max_fwd (x : u32) (y : u32) : u32 result =
+    if u32_ge x y then Return x else Return y
+’
+
+val test3_fwd_def = Define ‘
+  (** [no_nested_borrows::test3]: forward function *)
+  test3_fwd : unit result =
+    do
+    x <- get_max_fwd (int_to_u32 4) (int_to_u32 3);
+    y <- get_max_fwd (int_to_u32 10) (int_to_u32 11);
+    z <- u32_add x y;
+    if ~ (z = int_to_u32 15) then Fail Failure else Return ()
+    od
+’
+
+(** Unit test for [no_nested_borrows::test3] *)
+val _ = assert_return (“test3_fwd”)
+
+val test_neg1_fwd_def = Define ‘
+  (** [no_nested_borrows::test_neg1]: forward function *)
+  test_neg1_fwd : unit result =
+    do
+    y <- i32_neg (int_to_i32 3);
+    if ~ (y = int_to_i32 (-3)) then Fail Failure else Return ()
+    od
+’
+
+(** Unit test for [no_nested_borrows::test_neg1] *)
+val _ = assert_return (“test_neg1_fwd”)
+
+val refs_test1_fwd_def = Define ‘
+  (** [no_nested_borrows::refs_test1]: forward function *)
+  refs_test1_fwd : unit result =
+    if ~ (int_to_i32 1 = int_to_i32 1) then Fail Failure else Return ()
+’
+
+(** Unit test for [no_nested_borrows::refs_test1] *)
+val _ = assert_return (“refs_test1_fwd”)
+
+val refs_test2_fwd_def = Define ‘
+  (** [no_nested_borrows::refs_test2]: forward function *)
+  refs_test2_fwd : unit result =
+    if ~ (int_to_i32 2 = int_to_i32 2)
+    then Fail Failure
+    else
+      if ~ (int_to_i32 0 = int_to_i32 0)
+      then Fail Failure
+      else
+        if ~ (int_to_i32 2 = int_to_i32 2)
+        then Fail Failure
+        else
+          if ~ (int_to_i32 2 = int_to_i32 2) then Fail Failure else Return ()
+’
+
+(** Unit test for [no_nested_borrows::refs_test2] *)
+val _ = assert_return (“refs_test2_fwd”)
+
+val test_list1_fwd_def = Define ‘
+  (** [no_nested_borrows::test_list1]: forward function *)
+  test_list1_fwd : unit result =
+    Return ()
+’
+
+(** Unit test for [no_nested_borrows::test_list1] *)
+val _ = assert_return (“test_list1_fwd”)
+
+val test_box1_fwd_def = Define ‘
+  (** [no_nested_borrows::test_box1]: forward function *)
+  test_box1_fwd : unit result =
+    let b = int_to_i32 1 in
+    let x = b in
+    if ~ (x = int_to_i32 1) then Fail Failure else Return ()
+’
+
+(** Unit test for [no_nested_borrows::test_box1] *)
+val _ = assert_return (“test_box1_fwd”)
+
+val copy_int_fwd_def = Define ‘
+  (** [no_nested_borrows::copy_int]: forward function *)
+  copy_int_fwd (x : i32) : i32 result =
+    Return x
+’
+
+val test_unreachable_fwd_def = Define ‘
+  (** [no_nested_borrows::test_unreachable]: forward function *)
+  test_unreachable_fwd (b : bool) : unit result =
+    if b then Fail Failure else Return ()
+’
+
+val test_panic_fwd_def = Define ‘
+  (** [no_nested_borrows::test_panic]: forward function *)
+  test_panic_fwd (b : bool) : unit result =
+    if b then Fail Failure else Return ()
+’
+
+val test_copy_int_fwd_def = Define ‘
+  (** [no_nested_borrows::test_copy_int]: forward function *)
+  test_copy_int_fwd : unit result =
+    do
+    y <- copy_int_fwd (int_to_i32 0);
+    if ~ (int_to_i32 0 = y) then Fail Failure else Return ()
+    od
+’
+
+(** Unit test for [no_nested_borrows::test_copy_int] *)
+val _ = assert_return (“test_copy_int_fwd”)
+
+val is_cons_fwd_def = Define ‘
+  (** [no_nested_borrows::is_cons]: forward function *)
+  is_cons_fwd (l : 't list_t) : bool result =
+    (case l of | ListCons t l0 => Return T | ListNil => Return F)
+’
+
+val test_is_cons_fwd_def = Define ‘
+  (** [no_nested_borrows::test_is_cons]: forward function *)
+  test_is_cons_fwd : unit result =
+    let l = ListNil in
+    do
+    b <- is_cons_fwd (ListCons (int_to_i32 0) l);
+    if ~ b then Fail Failure else Return ()
+    od
+’
+
+(** Unit test for [no_nested_borrows::test_is_cons] *)
+val _ = assert_return (“test_is_cons_fwd”)
+
+val split_list_fwd_def = Define ‘
+  (** [no_nested_borrows::split_list]: forward function *)
+  split_list_fwd (l : 't list_t) : ('t # 't list_t) result =
+    (case l of | ListCons hd tl => Return (hd, tl) | ListNil => Fail Failure)
+’
+
+val test_split_list_fwd_def = Define ‘
+  (** [no_nested_borrows::test_split_list]: forward function *)
+  test_split_list_fwd : unit result =
+    let l = ListNil in
+    do
+    p <- split_list_fwd (ListCons (int_to_i32 0) l);
+    let (hd, _) = p in
+    if ~ (hd = int_to_i32 0) then Fail Failure else Return ()
+    od
+’
+
+(** Unit test for [no_nested_borrows::test_split_list] *)
+val _ = assert_return (“test_split_list_fwd”)
+
+val choose_fwd_def = Define ‘
+  (** [no_nested_borrows::choose]: forward function *)
+  choose_fwd (b : bool) (x : 't) (y : 't) : 't result =
+    if b then Return x else Return y
+’
+
+val choose_back_def = Define ‘
+  (** [no_nested_borrows::choose]: backward function 0 *)
+  choose_back (b : bool) (x : 't) (y : 't) (ret : 't) : ('t # 't) result =
+    if b then Return (ret, y) else Return (x, ret)
+’
+
+val choose_test_fwd_def = Define ‘
+  (** [no_nested_borrows::choose_test]: forward function *)
+  choose_test_fwd : unit result =
+    do
+    z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
+    z0 <- i32_add z (int_to_i32 1);
+    if ~ (z0 = int_to_i32 1)
+    then Fail Failure
+    else (
+      do
+      (x, y) <- choose_back T (int_to_i32 0) (int_to_i32 0) z0;
+      if ~ (x = int_to_i32 1)
+      then Fail Failure
+      else if ~ (y = int_to_i32 0) then Fail Failure else Return ()
+      od)
+    od
+’
+
+(** Unit test for [no_nested_borrows::choose_test] *)
+val _ = assert_return (“choose_test_fwd”)
+
+val test_char_fwd_def = Define ‘
+  (** [no_nested_borrows::test_char]: forward function *)
+  test_char_fwd : char result =
+    Return #"a"
+’
+
+Datatype:
+  (** [no_nested_borrows::Tree] *)
+  tree_t = | TreeLeaf 't | TreeNode 't node_elem_t tree_t ;
+  
+  (** [no_nested_borrows::NodeElem] *)
+  node_elem_t = | NodeElemCons tree_t node_elem_t | NodeElemNil
+End
+
+val [list_length_fwd_def] = DefineDiv ‘
+  (** [no_nested_borrows::list_length]: forward function *)
+  list_length_fwd (l : 't list_t) : u32 result =
+    (case l of
+    | ListCons t l1 => do
+                       i <- list_length_fwd l1;
+                       u32_add (int_to_u32 1) i
+                       od
+    | ListNil => Return (int_to_u32 0))
+’
+
+val [list_nth_shared_fwd_def] = DefineDiv ‘
+  (** [no_nested_borrows::list_nth_shared]: forward function *)
+  list_nth_shared_fwd (l : 't list_t) (i : u32) : 't result =
+    (case l of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return x
+      else (do
+            i0 <- u32_sub i (int_to_u32 1);
+            list_nth_shared_fwd tl i0
+            od)
+    | ListNil => Fail Failure)
+’
+
+val [list_nth_mut_fwd_def] = DefineDiv ‘
+  (** [no_nested_borrows::list_nth_mut]: forward function *)
+  list_nth_mut_fwd (l : 't list_t) (i : u32) : 't result =
+    (case l of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return x
+      else (do
+            i0 <- u32_sub i (int_to_u32 1);
+            list_nth_mut_fwd tl i0
+            od)
+    | ListNil => Fail Failure)
+’
+
+val [list_nth_mut_back_def] = DefineDiv ‘
+  (** [no_nested_borrows::list_nth_mut]: backward function 0 *)
+  list_nth_mut_back (l : 't list_t) (i : u32) (ret : 't) : 't list_t result =
+    (case l of
+    | ListCons x tl =>
+      if i = int_to_u32 0
+      then Return (ListCons ret tl)
+      else (
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        tl0 <- list_nth_mut_back tl i0 ret;
+        Return (ListCons x tl0)
+        od)
+    | ListNil => Fail Failure)
+’
+
+val [list_rev_aux_fwd_def] = DefineDiv ‘
+  (** [no_nested_borrows::list_rev_aux]: forward function *)
+  list_rev_aux_fwd (li : 't list_t) (lo : 't list_t) : 't list_t result =
+    (case li of
+    | ListCons hd tl => list_rev_aux_fwd tl (ListCons hd lo)
+    | ListNil => Return lo)
+’
+
+val list_rev_fwd_back_def = Define ‘
+  (** [no_nested_borrows::list_rev]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
+  list_rev_fwd_back (l : 't list_t) : 't list_t result =
+    let li = mem_replace_fwd l ListNil in list_rev_aux_fwd li ListNil
+’
+
+val test_list_functions_fwd_def = Define ‘
+  (** [no_nested_borrows::test_list_functions]: forward function *)
+  test_list_functions_fwd : unit result =
+    let l = ListNil in
+    let l0 = ListCons (int_to_i32 2) l in
+    let l1 = ListCons (int_to_i32 1) l0 in
+    do
+    i <- list_length_fwd (ListCons (int_to_i32 0) l1);
+    if ~ (i = int_to_u32 3)
+    then Fail Failure
+    else (
+      do
+      i0 <- list_nth_shared_fwd (ListCons (int_to_i32 0) l1) (int_to_u32 0);
+      if ~ (i0 = int_to_i32 0)
+      then Fail Failure
+      else (
+        do
+        i1 <- list_nth_shared_fwd (ListCons (int_to_i32 0) l1) (int_to_u32 1);
+        if ~ (i1 = int_to_i32 1)
+        then Fail Failure
+        else (
+          do
+          i2 <-
+            list_nth_shared_fwd (ListCons (int_to_i32 0) l1) (int_to_u32 2);
+          if ~ (i2 = int_to_i32 2)
+          then Fail Failure
+          else (
+            do
+            ls <-
+              list_nth_mut_back (ListCons (int_to_i32 0) l1) (int_to_u32 1)
+                (int_to_i32 3);
+            i3 <- list_nth_shared_fwd ls (int_to_u32 0);
+            if ~ (i3 = int_to_i32 0)
+            then Fail Failure
+            else (
+              do
+              i4 <- list_nth_shared_fwd ls (int_to_u32 1);
+              if ~ (i4 = int_to_i32 3)
+              then Fail Failure
+              else (
+                do
+                i5 <- list_nth_shared_fwd ls (int_to_u32 2);
+                if ~ (i5 = int_to_i32 2) then Fail Failure else Return ()
+                od)
+              od)
+            od)
+          od)
+        od)
+      od)
+    od
+’
+
+(** Unit test for [no_nested_borrows::test_list_functions] *)
+val _ = assert_return (“test_list_functions_fwd”)
+
+val id_mut_pair1_fwd_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair1]: forward function *)
+  id_mut_pair1_fwd (x : 't1) (y : 't2) : ('t1 # 't2) result =
+    Return (x, y)
+’
+
+val id_mut_pair1_back_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair1]: backward function 0 *)
+  id_mut_pair1_back
+    (x : 't1) (y : 't2) (ret : ('t1 # 't2)) : ('t1 # 't2) result =
+    let (t, t0) = ret in Return (t, t0)
+’
+
+val id_mut_pair2_fwd_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair2]: forward function *)
+  id_mut_pair2_fwd (p : ('t1 # 't2)) : ('t1 # 't2) result =
+    let (t, t0) = p in Return (t, t0)
+’
+
+val id_mut_pair2_back_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair2]: backward function 0 *)
+  id_mut_pair2_back
+    (p : ('t1 # 't2)) (ret : ('t1 # 't2)) : ('t1 # 't2) result =
+    let (t, t0) = ret in Return (t, t0)
+’
+
+val id_mut_pair3_fwd_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair3]: forward function *)
+  id_mut_pair3_fwd (x : 't1) (y : 't2) : ('t1 # 't2) result =
+    Return (x, y)
+’
+
+val id_mut_pair3_back'a_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair3]: backward function 0 *)
+  id_mut_pair3_back'a (x : 't1) (y : 't2) (ret : 't1) : 't1 result =
+    Return ret
+’
+
+val id_mut_pair3_back'b_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair3]: backward function 1 *)
+  id_mut_pair3_back'b (x : 't1) (y : 't2) (ret : 't2) : 't2 result =
+    Return ret
+’
+
+val id_mut_pair4_fwd_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair4]: forward function *)
+  id_mut_pair4_fwd (p : ('t1 # 't2)) : ('t1 # 't2) result =
+    let (t, t0) = p in Return (t, t0)
+’
+
+val id_mut_pair4_back'a_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair4]: backward function 0 *)
+  id_mut_pair4_back'a (p : ('t1 # 't2)) (ret : 't1) : 't1 result =
+    Return ret
+’
+
+val id_mut_pair4_back'b_def = Define ‘
+  (** [no_nested_borrows::id_mut_pair4]: backward function 1 *)
+  id_mut_pair4_back'b (p : ('t1 # 't2)) (ret : 't2) : 't2 result =
+    Return ret
+’
+
+Datatype:
+  (** [no_nested_borrows::StructWithTuple] *)
+  struct_with_tuple_t = <| struct_with_tuple_p : ('t1 # 't2); |>
+End
+
+val new_tuple1_fwd_def = Define ‘
+  (** [no_nested_borrows::new_tuple1]: forward function *)
+  new_tuple1_fwd : (u32, u32) struct_with_tuple_t result =
+    Return (<| struct_with_tuple_p := (int_to_u32 1, int_to_u32 2) |>)
+’
+
+val new_tuple2_fwd_def = Define ‘
+  (** [no_nested_borrows::new_tuple2]: forward function *)
+  new_tuple2_fwd : (i16, i16) struct_with_tuple_t result =
+    Return (<| struct_with_tuple_p := (int_to_i16 1, int_to_i16 2) |>)
+’
+
+val new_tuple3_fwd_def = Define ‘
+  (** [no_nested_borrows::new_tuple3]: forward function *)
+  new_tuple3_fwd : (u64, i64) struct_with_tuple_t result =
+    Return (<| struct_with_tuple_p := (int_to_u64 1, int_to_i64 2) |>)
+’
+
+Datatype:
+  (** [no_nested_borrows::StructWithPair] *)
+  struct_with_pair_t = <| struct_with_pair_p : ('t1, 't2) pair_t; |>
+End
+
+val new_pair1_fwd_def = Define ‘
+  (** [no_nested_borrows::new_pair1]: forward function *)
+  new_pair1_fwd : (u32, u32) struct_with_pair_t result =
+    Return
+    (<|
+       struct_with_pair_p :=
+         (<| pair_x := (int_to_u32 1); pair_y := (int_to_u32 2) |>)
+       |>)
+’
+
+val test_constants_fwd_def = Define ‘
+  (** [no_nested_borrows::test_constants]: forward function *)
+  test_constants_fwd : unit result =
+    do
+    swt <- new_tuple1_fwd;
+    let (i, _) = swt.struct_with_tuple_p in
+    if ~ (i = int_to_u32 1)
+    then Fail Failure
+    else (
+      do
+      swt0 <- new_tuple2_fwd;
+      let (i0, _) = swt0.struct_with_tuple_p in
+      if ~ (i0 = int_to_i16 1)
+      then Fail Failure
+      else (
+        do
+        swt1 <- new_tuple3_fwd;
+        let (i1, _) = swt1.struct_with_tuple_p in
+        if ~ (i1 = int_to_u64 1)
+        then Fail Failure
+        else (
+          do
+          swp <- new_pair1_fwd;
+          if ~ (swp.struct_with_pair_p.pair_x = int_to_u32 1)
+          then Fail Failure
+          else Return ()
+          od)
+        od)
+      od)
+    od
+’
+
+(** Unit test for [no_nested_borrows::test_constants] *)
+val _ = assert_return (“test_constants_fwd”)
+
+val test_weird_borrows1_fwd_def = Define ‘
+  (** [no_nested_borrows::test_weird_borrows1]: forward function *)
+  test_weird_borrows1_fwd : unit result =
+    Return ()
+’
+
+(** Unit test for [no_nested_borrows::test_weird_borrows1] *)
+val _ = assert_return (“test_weird_borrows1_fwd”)
+
+val test_mem_replace_fwd_back_def = Define ‘
+  (** [no_nested_borrows::test_mem_replace]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
+  test_mem_replace_fwd_back (px : u32) : u32 result =
+    let y = mem_replace_fwd px (int_to_u32 1) in
+    if ~ (y = int_to_u32 0) then Fail Failure else Return (int_to_u32 2)
+’
+
+val test_shared_borrow_bool1_fwd_def = Define ‘
+  (** [no_nested_borrows::test_shared_borrow_bool1]: forward function *)
+  test_shared_borrow_bool1_fwd (b : bool) : u32 result =
+    if b then Return (int_to_u32 0) else Return (int_to_u32 1)
+’
+
+val test_shared_borrow_bool2_fwd_def = Define ‘
+  (** [no_nested_borrows::test_shared_borrow_bool2]: forward function *)
+  test_shared_borrow_bool2_fwd : u32 result =
+    Return (int_to_u32 0)
+’
+
+val test_shared_borrow_enum1_fwd_def = Define ‘
+  (** [no_nested_borrows::test_shared_borrow_enum1]: forward function *)
+  test_shared_borrow_enum1_fwd (l : u32 list_t) : u32 result =
+    (case l of
+    | ListCons i l0 => Return (int_to_u32 1)
+    | ListNil => Return (int_to_u32 0))
+’
+
+val test_shared_borrow_enum2_fwd_def = Define ‘
+  (** [no_nested_borrows::test_shared_borrow_enum2]: forward function *)
+  test_shared_borrow_enum2_fwd : u32 result =
+    Return (int_to_u32 0)
+’
+
+val _ = export_theory ()
diff --git a/tests/hol4/no_nested_borrows/noNestedBorrowsTheory.sig b/tests/hol4/no_nested_borrows/noNestedBorrowsTheory.sig
new file mode 100644
index 00000000..67368e38
--- /dev/null
+++ b/tests/hol4/no_nested_borrows/noNestedBorrowsTheory.sig
@@ -0,0 +1,1598 @@
+signature noNestedBorrowsTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val add_test_fwd_def : thm
+    val cast_test_fwd_def : thm
+    val choose_back_def : thm
+    val choose_fwd_def : thm
+    val choose_test_fwd_def : thm
+    val copy_int_fwd_def : thm
+    val div_test1_fwd_def : thm
+    val div_test_fwd_def : thm
+    val empty_enum_t_BIJ : thm
+    val empty_enum_t_CASE : thm
+    val empty_enum_t_TY_DEF : thm
+    val empty_enum_t_size_def : thm
+    val enum_t_BIJ : thm
+    val enum_t_CASE : thm
+    val enum_t_TY_DEF : thm
+    val enum_t_size_def : thm
+    val get_max_fwd_def : thm
+    val id_mut_pair1_back_def : thm
+    val id_mut_pair1_fwd_def : thm
+    val id_mut_pair2_back_def : thm
+    val id_mut_pair2_fwd_def : thm
+    val id_mut_pair3_back'a_def : thm
+    val id_mut_pair3_back'b_def : thm
+    val id_mut_pair3_fwd_def : thm
+    val id_mut_pair4_back'a_def : thm
+    val id_mut_pair4_back'b_def : thm
+    val id_mut_pair4_fwd_def : thm
+    val is_cons_fwd_def : thm
+    val list_length_fwd_def : thm
+    val list_nth_mut_back_def : thm
+    val list_nth_mut_fwd_def : thm
+    val list_nth_shared_fwd_def : thm
+    val list_rev_aux_fwd_def : thm
+    val list_rev_fwd_back_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val neg_test_fwd_def : thm
+    val new_pair1_fwd_def : thm
+    val new_tuple1_fwd_def : thm
+    val new_tuple2_fwd_def : thm
+    val new_tuple3_fwd_def : thm
+    val node_elem_t_TY_DEF : thm
+    val node_elem_t_case_def : thm
+    val one_t_TY_DEF : thm
+    val one_t_case_def : thm
+    val one_t_size_def : thm
+    val pair_t_TY_DEF : thm
+    val pair_t_case_def : thm
+    val pair_t_pair_x : thm
+    val pair_t_pair_x_fupd : thm
+    val pair_t_pair_y : thm
+    val pair_t_pair_y_fupd : thm
+    val pair_t_size_def : thm
+    val refs_test1_fwd_def : thm
+    val refs_test2_fwd_def : thm
+    val rem_test_fwd_def : thm
+    val split_list_fwd_def : thm
+    val struct_with_pair_t_TY_DEF : thm
+    val struct_with_pair_t_case_def : thm
+    val struct_with_pair_t_size_def : thm
+    val struct_with_pair_t_struct_with_pair_p : thm
+    val struct_with_pair_t_struct_with_pair_p_fupd : thm
+    val struct_with_tuple_t_TY_DEF : thm
+    val struct_with_tuple_t_case_def : thm
+    val struct_with_tuple_t_size_def : thm
+    val struct_with_tuple_t_struct_with_tuple_p : thm
+    val struct_with_tuple_t_struct_with_tuple_p_fupd : thm
+    val subs_test_fwd_def : thm
+    val sum_t_TY_DEF : thm
+    val sum_t_case_def : thm
+    val sum_t_size_def : thm
+    val test2_fwd_def : thm
+    val test3_fwd_def : thm
+    val test_box1_fwd_def : thm
+    val test_char_fwd_def : thm
+    val test_constants_fwd_def : thm
+    val test_copy_int_fwd_def : thm
+    val test_is_cons_fwd_def : thm
+    val test_list1_fwd_def : thm
+    val test_list_functions_fwd_def : thm
+    val test_mem_replace_fwd_back_def : thm
+    val test_neg1_fwd_def : thm
+    val test_panic_fwd_def : thm
+    val test_shared_borrow_bool1_fwd_def : thm
+    val test_shared_borrow_bool2_fwd_def : thm
+    val test_shared_borrow_enum1_fwd_def : thm
+    val test_shared_borrow_enum2_fwd_def : thm
+    val test_split_list_fwd_def : thm
+    val test_unreachable_fwd_def : thm
+    val test_weird_borrows1_fwd_def : thm
+    val tree_t_TY_DEF : thm
+    val tree_t_case_def : thm
+    val tree_t_size_def : thm
+  
+  (*  Theorems  *)
+    val EXISTS_pair_t : thm
+    val EXISTS_struct_with_pair_t : thm
+    val EXISTS_struct_with_tuple_t : thm
+    val FORALL_pair_t : thm
+    val FORALL_struct_with_pair_t : thm
+    val FORALL_struct_with_tuple_t : thm
+    val datatype_empty_enum_t : thm
+    val datatype_enum_t : thm
+    val datatype_list_t : thm
+    val datatype_one_t : thm
+    val datatype_pair_t : thm
+    val datatype_struct_with_pair_t : thm
+    val datatype_struct_with_tuple_t : thm
+    val datatype_sum_t : thm
+    val datatype_tree_t : thm
+    val empty_enum_t2num_11 : thm
+    val empty_enum_t2num_ONTO : thm
+    val empty_enum_t2num_num2empty_enum_t : thm
+    val empty_enum_t2num_thm : thm
+    val empty_enum_t_Axiom : thm
+    val empty_enum_t_EQ_empty_enum_t : thm
+    val empty_enum_t_case_cong : thm
+    val empty_enum_t_case_def : thm
+    val empty_enum_t_case_eq : thm
+    val empty_enum_t_induction : thm
+    val empty_enum_t_nchotomy : thm
+    val enum_t2num_11 : thm
+    val enum_t2num_ONTO : thm
+    val enum_t2num_num2enum_t : thm
+    val enum_t2num_thm : thm
+    val enum_t_Axiom : thm
+    val enum_t_EQ_enum_t : thm
+    val enum_t_case_cong : thm
+    val enum_t_case_def : thm
+    val enum_t_case_eq : thm
+    val enum_t_distinct : thm
+    val enum_t_induction : thm
+    val enum_t_nchotomy : thm
+    val list_t_11 : thm
+    val list_t_Axiom : thm
+    val list_t_case_cong : thm
+    val list_t_case_eq : thm
+    val list_t_distinct : thm
+    val list_t_induction : thm
+    val list_t_nchotomy : thm
+    val node_elem_t_11 : thm
+    val node_elem_t_Axiom : thm
+    val node_elem_t_case_cong : thm
+    val node_elem_t_case_eq : thm
+    val node_elem_t_distinct : thm
+    val node_elem_t_induction : thm
+    val node_elem_t_nchotomy : thm
+    val num2empty_enum_t_11 : thm
+    val num2empty_enum_t_ONTO : thm
+    val num2empty_enum_t_empty_enum_t2num : thm
+    val num2empty_enum_t_thm : thm
+    val num2enum_t_11 : thm
+    val num2enum_t_ONTO : thm
+    val num2enum_t_enum_t2num : thm
+    val num2enum_t_thm : thm
+    val one_t_11 : thm
+    val one_t_Axiom : thm
+    val one_t_case_cong : thm
+    val one_t_case_eq : thm
+    val one_t_induction : thm
+    val one_t_nchotomy : thm
+    val pair_t_11 : thm
+    val pair_t_Axiom : thm
+    val pair_t_accessors : thm
+    val pair_t_accfupds : thm
+    val pair_t_case_cong : thm
+    val pair_t_case_eq : thm
+    val pair_t_component_equality : thm
+    val pair_t_fn_updates : thm
+    val pair_t_fupdcanon : thm
+    val pair_t_fupdcanon_comp : thm
+    val pair_t_fupdfupds : thm
+    val pair_t_fupdfupds_comp : thm
+    val pair_t_induction : thm
+    val pair_t_literal_11 : thm
+    val pair_t_literal_nchotomy : thm
+    val pair_t_nchotomy : thm
+    val pair_t_updates_eq_literal : thm
+    val struct_with_pair_t_11 : thm
+    val struct_with_pair_t_Axiom : thm
+    val struct_with_pair_t_accessors : thm
+    val struct_with_pair_t_accfupds : thm
+    val struct_with_pair_t_case_cong : thm
+    val struct_with_pair_t_case_eq : thm
+    val struct_with_pair_t_component_equality : thm
+    val struct_with_pair_t_fn_updates : thm
+    val struct_with_pair_t_fupdfupds : thm
+    val struct_with_pair_t_fupdfupds_comp : thm
+    val struct_with_pair_t_induction : thm
+    val struct_with_pair_t_literal_11 : thm
+    val struct_with_pair_t_literal_nchotomy : thm
+    val struct_with_pair_t_nchotomy : thm
+    val struct_with_pair_t_updates_eq_literal : thm
+    val struct_with_tuple_t_11 : thm
+    val struct_with_tuple_t_Axiom : thm
+    val struct_with_tuple_t_accessors : thm
+    val struct_with_tuple_t_accfupds : thm
+    val struct_with_tuple_t_case_cong : thm
+    val struct_with_tuple_t_case_eq : thm
+    val struct_with_tuple_t_component_equality : thm
+    val struct_with_tuple_t_fn_updates : thm
+    val struct_with_tuple_t_fupdfupds : thm
+    val struct_with_tuple_t_fupdfupds_comp : thm
+    val struct_with_tuple_t_induction : thm
+    val struct_with_tuple_t_literal_11 : thm
+    val struct_with_tuple_t_literal_nchotomy : thm
+    val struct_with_tuple_t_nchotomy : thm
+    val struct_with_tuple_t_updates_eq_literal : thm
+    val sum_t_11 : thm
+    val sum_t_Axiom : thm
+    val sum_t_case_cong : thm
+    val sum_t_case_eq : thm
+    val sum_t_distinct : thm
+    val sum_t_induction : thm
+    val sum_t_nchotomy : thm
+    val tree_t_11 : thm
+    val tree_t_Axiom : thm
+    val tree_t_case_cong : thm
+    val tree_t_case_eq : thm
+    val tree_t_distinct : thm
+    val tree_t_induction : thm
+    val tree_t_nchotomy : thm
+  
+  val noNestedBorrows_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [divDef] Parent theory of "noNestedBorrows"
+   
+   [add_test_fwd_def]  Definition
+      
+      ⊢ ∀x y. add_test_fwd x y = u32_add x y
+   
+   [cast_test_fwd_def]  Definition
+      
+      ⊢ ∀x. cast_test_fwd x = mk_i32 (u32_to_int x)
+   
+   [choose_back_def]  Definition
+      
+      ⊢ ∀b x y ret.
+          choose_back b x y ret =
+          if b then Return (ret,y) else Return (x,ret)
+   
+   [choose_fwd_def]  Definition
+      
+      ⊢ ∀b x y. choose_fwd b x y = if b then Return x else Return y
+   
+   [choose_test_fwd_def]  Definition
+      
+      ⊢ choose_test_fwd =
+        do
+          z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
+          z0 <- i32_add z (int_to_i32 1);
+          if z0 ≠ int_to_i32 1 then Fail Failure
+          else
+            do
+              (x,y) <- choose_back T (int_to_i32 0) (int_to_i32 0) z0;
+              if x ≠ int_to_i32 1 then Fail Failure
+              else if y ≠ int_to_i32 0 then Fail Failure
+              else Return ()
+            od
+        od
+   
+   [copy_int_fwd_def]  Definition
+      
+      ⊢ ∀x. copy_int_fwd x = Return x
+   
+   [div_test1_fwd_def]  Definition
+      
+      ⊢ ∀x. div_test1_fwd x = u32_div x (int_to_u32 2)
+   
+   [div_test_fwd_def]  Definition
+      
+      ⊢ ∀x y. div_test_fwd x y = u32_div x y
+   
+   [empty_enum_t_BIJ]  Definition
+      
+      ⊢ (∀a. num2empty_enum_t (empty_enum_t2num a) = a) ∧
+        ∀r. (λn. n < 1) r ⇔ empty_enum_t2num (num2empty_enum_t r) = r
+   
+   [empty_enum_t_CASE]  Definition
+      
+      ⊢ ∀x v0.
+          (case x of EmptyEnumEmpty => v0) = (λm. v0) (empty_enum_t2num x)
+   
+   [empty_enum_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep. TYPE_DEFINITION (λn. n < 1) rep
+   
+   [empty_enum_t_size_def]  Definition
+      
+      ⊢ ∀x. empty_enum_t_size x = 0
+   
+   [enum_t_BIJ]  Definition
+      
+      ⊢ (∀a. num2enum_t (enum_t2num a) = a) ∧
+        ∀r. (λn. n < 2) r ⇔ enum_t2num (num2enum_t r) = r
+   
+   [enum_t_CASE]  Definition
+      
+      ⊢ ∀x v0 v1.
+          (case x of EnumVariant1 => v0 | EnumVariant2 => v1) =
+          (λm. if m = 0 then v0 else v1) (enum_t2num x)
+   
+   [enum_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep. TYPE_DEFINITION (λn. n < 2) rep
+   
+   [enum_t_size_def]  Definition
+      
+      ⊢ ∀x. enum_t_size x = 0
+   
+   [get_max_fwd_def]  Definition
+      
+      ⊢ ∀x y. get_max_fwd x y = if u32_ge x y then Return x else Return y
+   
+   [id_mut_pair1_back_def]  Definition
+      
+      ⊢ ∀x y ret.
+          id_mut_pair1_back x y ret = (let (t,t0) = ret in Return (t,t0))
+   
+   [id_mut_pair1_fwd_def]  Definition
+      
+      ⊢ ∀x y. id_mut_pair1_fwd x y = Return (x,y)
+   
+   [id_mut_pair2_back_def]  Definition
+      
+      ⊢ ∀p ret.
+          id_mut_pair2_back p ret = (let (t,t0) = ret in Return (t,t0))
+   
+   [id_mut_pair2_fwd_def]  Definition
+      
+      ⊢ ∀p. id_mut_pair2_fwd p = (let (t,t0) = p in Return (t,t0))
+   
+   [id_mut_pair3_back'a_def]  Definition
+      
+      ⊢ ∀x y ret. id_mut_pair3_back'a x y ret = Return ret
+   
+   [id_mut_pair3_back'b_def]  Definition
+      
+      ⊢ ∀x y ret. id_mut_pair3_back'b x y ret = Return ret
+   
+   [id_mut_pair3_fwd_def]  Definition
+      
+      ⊢ ∀x y. id_mut_pair3_fwd x y = Return (x,y)
+   
+   [id_mut_pair4_back'a_def]  Definition
+      
+      ⊢ ∀p ret. id_mut_pair4_back'a p ret = Return ret
+   
+   [id_mut_pair4_back'b_def]  Definition
+      
+      ⊢ ∀p ret. id_mut_pair4_back'b p ret = Return ret
+   
+   [id_mut_pair4_fwd_def]  Definition
+      
+      ⊢ ∀p. id_mut_pair4_fwd p = (let (t,t0) = p in Return (t,t0))
+   
+   [is_cons_fwd_def]  Definition
+      
+      ⊢ ∀l. is_cons_fwd l =
+            case l of ListCons t l0 => Return T | ListNil => Return F
+   
+   [list_length_fwd_def]  Definition
+      
+      ⊢ ∀l. list_length_fwd l =
+            case l of
+              ListCons t l1 =>
+                do i <- list_length_fwd l1; u32_add (int_to_u32 1) i od
+            | ListNil => Return (int_to_u32 0)
+   
+   [list_nth_mut_back_def]  Definition
+      
+      ⊢ ∀l i ret.
+          list_nth_mut_back l i ret =
+          case l of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return (ListCons ret tl)
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  tl0 <- list_nth_mut_back tl i0 ret;
+                  Return (ListCons x tl0)
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_mut_fwd_def]  Definition
+      
+      ⊢ ∀l i.
+          list_nth_mut_fwd l i =
+          case l of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return x
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  list_nth_mut_fwd tl i0
+                od
+          | ListNil => Fail Failure
+   
+   [list_nth_shared_fwd_def]  Definition
+      
+      ⊢ ∀l i.
+          list_nth_shared_fwd l i =
+          case l of
+            ListCons x tl =>
+              if i = int_to_u32 0 then Return x
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  list_nth_shared_fwd tl i0
+                od
+          | ListNil => Fail Failure
+   
+   [list_rev_aux_fwd_def]  Definition
+      
+      ⊢ ∀li lo.
+          list_rev_aux_fwd li lo =
+          case li of
+            ListCons hd tl => list_rev_aux_fwd tl (ListCons hd lo)
+          | ListNil => Return lo
+   
+   [list_rev_fwd_back_def]  Definition
+      
+      ⊢ ∀l. list_rev_fwd_back l =
+            (let
+               li = mem_replace_fwd l ListNil
+             in
+               list_rev_aux_fwd li ListNil)
+   
+   [list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('list_t').
+                   (∀a0'.
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR 0 a0
+                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+                           a0 a1 ∧ $var$('list_t') a1) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+                      $var$('list_t') a0') ⇒
+                   $var$('list_t') a0') rep
+   
+   [list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. list_t_CASE ListNil f v = v
+   
+   [list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1.
+           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+        ∀f. list_t_size f ListNil = 0
+   
+   [neg_test_fwd_def]  Definition
+      
+      ⊢ ∀x. neg_test_fwd x = i32_neg x
+   
+   [new_pair1_fwd_def]  Definition
+      
+      ⊢ new_pair1_fwd =
+        Return
+          <|struct_with_pair_p :=
+              <|pair_x := int_to_u32 1; pair_y := int_to_u32 2|> |>
+   
+   [new_tuple1_fwd_def]  Definition
+      
+      ⊢ new_tuple1_fwd =
+        Return <|struct_with_tuple_p := (int_to_u32 1,int_to_u32 2)|>
+   
+   [new_tuple2_fwd_def]  Definition
+      
+      ⊢ new_tuple2_fwd =
+        Return <|struct_with_tuple_p := (int_to_i16 1,int_to_i16 2)|>
+   
+   [new_tuple3_fwd_def]  Definition
+      
+      ⊢ new_tuple3_fwd =
+        Return <|struct_with_tuple_p := (int_to_u64 1,int_to_i64 2)|>
+   
+   [node_elem_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa1'.
+                 ∀ $var$('tree_t') $var$('node_elem_t').
+                   (∀a0'.
+                      (∃a. a0' =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ∨
+                      (∃a0 a1 a2.
+                         a0' =
+                         (λa0 a1 a2.
+                              ind_type$CONSTR (SUC 0) a0
+                                (ind_type$FCONS a1
+                                   (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
+                           a0 a1 a2 ∧ $var$('node_elem_t') a1 ∧
+                         $var$('tree_t') a2) ⇒
+                      $var$('tree_t') a0') ∧
+                   (∀a1'.
+                      (∃a0 a1.
+                         a1' =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC (SUC 0)) ARB
+                                (ind_type$FCONS a0
+                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+                           a0 a1 ∧ $var$('tree_t') a0 ∧
+                         $var$('node_elem_t') a1) ∨
+                      a1' =
+                      ind_type$CONSTR (SUC (SUC (SUC 0))) ARB
+                        (λn. ind_type$BOTTOM) ⇒
+                      $var$('node_elem_t') a1') ⇒
+                   $var$('node_elem_t') a1') rep
+   
+   [node_elem_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 f v. node_elem_t_CASE (NodeElemCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. node_elem_t_CASE NodeElemNil f v = v
+   
+   [one_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0.
+                 ∀ $var$('one_t').
+                   (∀a0.
+                      (∃a. a0 =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ⇒
+                      $var$('one_t') a0) ⇒
+                   $var$('one_t') a0) rep
+   
+   [one_t_case_def]  Definition
+      
+      ⊢ ∀a f. one_t_CASE (OneOne a) f = f a
+   
+   [one_t_size_def]  Definition
+      
+      ⊢ ∀f a. one_t_size f (OneOne a) = 1 + f a
+   
+   [pair_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('pair_t').
+                   (∀a0'.
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR 0 (a0,a1)
+                                (λn. ind_type$BOTTOM)) a0 a1) ⇒
+                      $var$('pair_t') a0') ⇒
+                   $var$('pair_t') a0') rep
+   
+   [pair_t_case_def]  Definition
+      
+      ⊢ ∀a0 a1 f. pair_t_CASE (pair_t a0 a1) f = f a0 a1
+   
+   [pair_t_pair_x]  Definition
+      
+      ⊢ ∀t t0. (pair_t t t0).pair_x = t
+   
+   [pair_t_pair_x_fupd]  Definition
+      
+      ⊢ ∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0
+   
+   [pair_t_pair_y]  Definition
+      
+      ⊢ ∀t t0. (pair_t t t0).pair_y = t0
+   
+   [pair_t_pair_y_fupd]  Definition
+      
+      ⊢ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0)
+   
+   [pair_t_size_def]  Definition
+      
+      ⊢ ∀f f1 a0 a1. pair_t_size f f1 (pair_t a0 a1) = 1 + (f a0 + f1 a1)
+   
+   [refs_test1_fwd_def]  Definition
+      
+      ⊢ refs_test1_fwd =
+        if int_to_i32 1 ≠ int_to_i32 1 then Fail Failure else Return ()
+   
+   [refs_test2_fwd_def]  Definition
+      
+      ⊢ refs_test2_fwd =
+        if int_to_i32 2 ≠ int_to_i32 2 then Fail Failure
+        else if int_to_i32 0 ≠ int_to_i32 0 then Fail Failure
+        else if int_to_i32 2 ≠ int_to_i32 2 then Fail Failure
+        else if int_to_i32 2 ≠ int_to_i32 2 then Fail Failure
+        else Return ()
+   
+   [rem_test_fwd_def]  Definition
+      
+      ⊢ ∀x y. rem_test_fwd x y = u32_rem x y
+   
+   [split_list_fwd_def]  Definition
+      
+      ⊢ ∀l. split_list_fwd l =
+            case l of
+              ListCons hd tl => Return (hd,tl)
+            | ListNil => Fail Failure
+   
+   [struct_with_pair_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0.
+                 ∀ $var$('struct_with_pair_t').
+                   (∀a0.
+                      (∃a. a0 =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ⇒
+                      $var$('struct_with_pair_t') a0) ⇒
+                   $var$('struct_with_pair_t') a0) rep
+   
+   [struct_with_pair_t_case_def]  Definition
+      
+      ⊢ ∀a f. struct_with_pair_t_CASE (struct_with_pair_t a) f = f a
+   
+   [struct_with_pair_t_size_def]  Definition
+      
+      ⊢ ∀f f1 a.
+          struct_with_pair_t_size f f1 (struct_with_pair_t a) =
+          1 + pair_t_size f f1 a
+   
+   [struct_with_pair_t_struct_with_pair_p]  Definition
+      
+      ⊢ ∀p. (struct_with_pair_t p).struct_with_pair_p = p
+   
+   [struct_with_pair_t_struct_with_pair_p_fupd]  Definition
+      
+      ⊢ ∀f p.
+          struct_with_pair_t p with struct_with_pair_p updated_by f =
+          struct_with_pair_t (f p)
+   
+   [struct_with_tuple_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0.
+                 ∀ $var$('struct_with_tuple_t').
+                   (∀a0.
+                      (∃a. a0 =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ⇒
+                      $var$('struct_with_tuple_t') a0) ⇒
+                   $var$('struct_with_tuple_t') a0) rep
+   
+   [struct_with_tuple_t_case_def]  Definition
+      
+      ⊢ ∀a f. struct_with_tuple_t_CASE (struct_with_tuple_t a) f = f a
+   
+   [struct_with_tuple_t_size_def]  Definition
+      
+      ⊢ ∀f f1 a.
+          struct_with_tuple_t_size f f1 (struct_with_tuple_t a) =
+          1 + pair_size f f1 a
+   
+   [struct_with_tuple_t_struct_with_tuple_p]  Definition
+      
+      ⊢ ∀p. (struct_with_tuple_t p).struct_with_tuple_p = p
+   
+   [struct_with_tuple_t_struct_with_tuple_p_fupd]  Definition
+      
+      ⊢ ∀f p.
+          struct_with_tuple_t p with struct_with_tuple_p updated_by f =
+          struct_with_tuple_t (f p)
+   
+   [subs_test_fwd_def]  Definition
+      
+      ⊢ ∀x y. subs_test_fwd x y = u32_sub x y
+   
+   [sum_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0.
+                 ∀ $var$('sum_t').
+                   (∀a0.
+                      (∃a. a0 =
+                           (λa.
+                                ind_type$CONSTR 0 (a,ARB)
+                                  (λn. ind_type$BOTTOM)) a) ∨
+                      (∃a. a0 =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) (ARB,a)
+                                  (λn. ind_type$BOTTOM)) a) ⇒
+                      $var$('sum_t') a0) ⇒
+                   $var$('sum_t') a0) rep
+   
+   [sum_t_case_def]  Definition
+      
+      ⊢ (∀a f f1. sum_t_CASE (SumLeft a) f f1 = f a) ∧
+        ∀a f f1. sum_t_CASE (SumRight a) f f1 = f1 a
+   
+   [sum_t_size_def]  Definition
+      
+      ⊢ (∀f f1 a. sum_t_size f f1 (SumLeft a) = 1 + f a) ∧
+        ∀f f1 a. sum_t_size f f1 (SumRight a) = 1 + f1 a
+   
+   [test2_fwd_def]  Definition
+      
+      ⊢ test2_fwd =
+        monad_ignore_bind (u32_add (int_to_u32 23) (int_to_u32 44))
+          (Return ())
+   
+   [test3_fwd_def]  Definition
+      
+      ⊢ test3_fwd =
+        do
+          x <- get_max_fwd (int_to_u32 4) (int_to_u32 3);
+          y <- get_max_fwd (int_to_u32 10) (int_to_u32 11);
+          z <- u32_add x y;
+          if z ≠ int_to_u32 15 then Fail Failure else Return ()
+        od
+   
+   [test_box1_fwd_def]  Definition
+      
+      ⊢ test_box1_fwd =
+        (let
+           b = int_to_i32 1;
+           x = b
+         in
+           if x ≠ int_to_i32 1 then Fail Failure else Return ())
+   
+   [test_char_fwd_def]  Definition
+      
+      ⊢ test_char_fwd = Return #"a"
+   
+   [test_constants_fwd_def]  Definition
+      
+      ⊢ test_constants_fwd =
+        do
+          swt <- new_tuple1_fwd;
+          (i,_) <<- swt.struct_with_tuple_p;
+          if i ≠ int_to_u32 1 then Fail Failure
+          else
+            do
+              swt0 <- new_tuple2_fwd;
+              (i0,_) <<- swt0.struct_with_tuple_p;
+              if i0 ≠ int_to_i16 1 then Fail Failure
+              else
+                do
+                  swt1 <- new_tuple3_fwd;
+                  (i1,_) <<- swt1.struct_with_tuple_p;
+                  if i1 ≠ int_to_u64 1 then Fail Failure
+                  else
+                    do
+                      swp <- new_pair1_fwd;
+                      if swp.struct_with_pair_p.pair_x ≠ int_to_u32 1 then
+                        Fail Failure
+                      else Return ()
+                    od
+                od
+            od
+        od
+   
+   [test_copy_int_fwd_def]  Definition
+      
+      ⊢ test_copy_int_fwd =
+        do
+          y <- copy_int_fwd (int_to_i32 0);
+          if int_to_i32 0 ≠ y then Fail Failure else Return ()
+        od
+   
+   [test_is_cons_fwd_def]  Definition
+      
+      ⊢ test_is_cons_fwd =
+        (let
+           l = ListNil
+         in
+           do
+             b <- is_cons_fwd (ListCons (int_to_i32 0) l);
+             if ¬b then Fail Failure else Return ()
+           od)
+   
+   [test_list1_fwd_def]  Definition
+      
+      ⊢ test_list1_fwd = Return ()
+   
+   [test_list_functions_fwd_def]  Definition
+      
+      ⊢ test_list_functions_fwd =
+        (let
+           l = ListNil;
+           l0 = ListCons (int_to_i32 2) l;
+           l1 = ListCons (int_to_i32 1) l0
+         in
+           do
+             i <- list_length_fwd (ListCons (int_to_i32 0) l1);
+             if i ≠ int_to_u32 3 then Fail Failure
+             else
+               do
+                 i0 <-
+                   list_nth_shared_fwd (ListCons (int_to_i32 0) l1)
+                     (int_to_u32 0);
+                 if i0 ≠ int_to_i32 0 then Fail Failure
+                 else
+                   do
+                     i1 <-
+                       list_nth_shared_fwd (ListCons (int_to_i32 0) l1)
+                         (int_to_u32 1);
+                     if i1 ≠ int_to_i32 1 then Fail Failure
+                     else
+                       do
+                         i2 <-
+                           list_nth_shared_fwd (ListCons (int_to_i32 0) l1)
+                             (int_to_u32 2);
+                         if i2 ≠ int_to_i32 2 then Fail Failure
+                         else
+                           do
+                             ls <-
+                               list_nth_mut_back
+                                 (ListCons (int_to_i32 0) l1)
+                                 (int_to_u32 1) (int_to_i32 3);
+                             i3 <- list_nth_shared_fwd ls (int_to_u32 0);
+                             if i3 ≠ int_to_i32 0 then Fail Failure
+                             else
+                               do
+                                 i4 <-
+                                   list_nth_shared_fwd ls (int_to_u32 1);
+                                 if i4 ≠ int_to_i32 3 then Fail Failure
+                                 else
+                                   do
+                                     i5 <-
+                                       list_nth_shared_fwd ls
+                                         (int_to_u32 2);
+                                     if i5 ≠ int_to_i32 2 then Fail Failure
+                                     else Return ()
+                                   od
+                               od
+                           od
+                       od
+                   od
+               od
+           od)
+   
+   [test_mem_replace_fwd_back_def]  Definition
+      
+      ⊢ ∀px.
+          test_mem_replace_fwd_back px =
+          (let
+             y = mem_replace_fwd px (int_to_u32 1)
+           in
+             if y ≠ int_to_u32 0 then Fail Failure
+             else Return (int_to_u32 2))
+   
+   [test_neg1_fwd_def]  Definition
+      
+      ⊢ test_neg1_fwd =
+        do
+          y <- i32_neg (int_to_i32 3);
+          if y ≠ int_to_i32 (-3) then Fail Failure else Return ()
+        od
+   
+   [test_panic_fwd_def]  Definition
+      
+      ⊢ ∀b. test_panic_fwd b = if b then Fail Failure else Return ()
+   
+   [test_shared_borrow_bool1_fwd_def]  Definition
+      
+      ⊢ ∀b. test_shared_borrow_bool1_fwd b =
+            if b then Return (int_to_u32 0) else Return (int_to_u32 1)
+   
+   [test_shared_borrow_bool2_fwd_def]  Definition
+      
+      ⊢ test_shared_borrow_bool2_fwd = Return (int_to_u32 0)
+   
+   [test_shared_borrow_enum1_fwd_def]  Definition
+      
+      ⊢ ∀l. test_shared_borrow_enum1_fwd l =
+            case l of
+              ListCons i l0 => Return (int_to_u32 1)
+            | ListNil => Return (int_to_u32 0)
+   
+   [test_shared_borrow_enum2_fwd_def]  Definition
+      
+      ⊢ test_shared_borrow_enum2_fwd = Return (int_to_u32 0)
+   
+   [test_split_list_fwd_def]  Definition
+      
+      ⊢ test_split_list_fwd =
+        (let
+           l = ListNil
+         in
+           do
+             p <- split_list_fwd (ListCons (int_to_i32 0) l);
+             (hd,_) <<- p;
+             if hd ≠ int_to_i32 0 then Fail Failure else Return ()
+           od)
+   
+   [test_unreachable_fwd_def]  Definition
+      
+      ⊢ ∀b. test_unreachable_fwd b = if b then Fail Failure else Return ()
+   
+   [test_weird_borrows1_fwd_def]  Definition
+      
+      ⊢ test_weird_borrows1_fwd = Return ()
+   
+   [tree_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('tree_t') $var$('node_elem_t').
+                   (∀a0'.
+                      (∃a. a0' =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ∨
+                      (∃a0 a1 a2.
+                         a0' =
+                         (λa0 a1 a2.
+                              ind_type$CONSTR (SUC 0) a0
+                                (ind_type$FCONS a1
+                                   (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
+                           a0 a1 a2 ∧ $var$('node_elem_t') a1 ∧
+                         $var$('tree_t') a2) ⇒
+                      $var$('tree_t') a0') ∧
+                   (∀a1'.
+                      (∃a0 a1.
+                         a1' =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC (SUC 0)) ARB
+                                (ind_type$FCONS a0
+                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+                           a0 a1 ∧ $var$('tree_t') a0 ∧
+                         $var$('node_elem_t') a1) ∨
+                      a1' =
+                      ind_type$CONSTR (SUC (SUC (SUC 0))) ARB
+                        (λn. ind_type$BOTTOM) ⇒
+                      $var$('node_elem_t') a1') ⇒
+                   $var$('tree_t') a0') rep
+   
+   [tree_t_case_def]  Definition
+      
+      ⊢ (∀a f f1. tree_t_CASE (TreeLeaf a) f f1 = f a) ∧
+        ∀a0 a1 a2 f f1. tree_t_CASE (TreeNode a0 a1 a2) f f1 = f1 a0 a1 a2
+   
+   [tree_t_size_def]  Definition
+      
+      ⊢ (∀f a. tree_t_size f (TreeLeaf a) = 1 + f a) ∧
+        (∀f a0 a1 a2.
+           tree_t_size f (TreeNode a0 a1 a2) =
+           1 + (f a0 + (node_elem_t_size f a1 + tree_t_size f a2))) ∧
+        (∀f a0 a1.
+           node_elem_t_size f (NodeElemCons a0 a1) =
+           1 + (tree_t_size f a0 + node_elem_t_size f a1)) ∧
+        ∀f. node_elem_t_size f NodeElemNil = 0
+   
+   [EXISTS_pair_t]  Theorem
+      
+      ⊢ ∀P. (∃p. P p) ⇔ ∃t0 t. P <|pair_x := t0; pair_y := t|>
+   
+   [EXISTS_struct_with_pair_t]  Theorem
+      
+      ⊢ ∀P. (∃s. P s) ⇔ ∃p. P <|struct_with_pair_p := p|>
+   
+   [EXISTS_struct_with_tuple_t]  Theorem
+      
+      ⊢ ∀P. (∃s. P s) ⇔ ∃p. P <|struct_with_tuple_p := p|>
+   
+   [FORALL_pair_t]  Theorem
+      
+      ⊢ ∀P. (∀p. P p) ⇔ ∀t0 t. P <|pair_x := t0; pair_y := t|>
+   
+   [FORALL_struct_with_pair_t]  Theorem
+      
+      ⊢ ∀P. (∀s. P s) ⇔ ∀p. P <|struct_with_pair_p := p|>
+   
+   [FORALL_struct_with_tuple_t]  Theorem
+      
+      ⊢ ∀P. (∀s. P s) ⇔ ∀p. P <|struct_with_tuple_p := p|>
+   
+   [datatype_empty_enum_t]  Theorem
+      
+      ⊢ DATATYPE (empty_enum_t EmptyEnumEmpty)
+   
+   [datatype_enum_t]  Theorem
+      
+      ⊢ DATATYPE (enum_t EnumVariant1 EnumVariant2)
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [datatype_one_t]  Theorem
+      
+      ⊢ DATATYPE (one_t OneOne)
+   
+   [datatype_pair_t]  Theorem
+      
+      ⊢ DATATYPE (record pair_t pair_x pair_y)
+   
+   [datatype_struct_with_pair_t]  Theorem
+      
+      ⊢ DATATYPE (record struct_with_pair_t struct_with_pair_p)
+   
+   [datatype_struct_with_tuple_t]  Theorem
+      
+      ⊢ DATATYPE (record struct_with_tuple_t struct_with_tuple_p)
+   
+   [datatype_sum_t]  Theorem
+      
+      ⊢ DATATYPE (sum_t SumLeft SumRight)
+   
+   [datatype_tree_t]  Theorem
+      
+      ⊢ DATATYPE
+          (tree_t TreeLeaf TreeNode ∧ node_elem_t NodeElemCons NodeElemNil)
+   
+   [empty_enum_t2num_11]  Theorem
+      
+      ⊢ ∀a a'. empty_enum_t2num a = empty_enum_t2num a' ⇔ a = a'
+   
+   [empty_enum_t2num_ONTO]  Theorem
+      
+      ⊢ ∀r. r < 1 ⇔ ∃a. r = empty_enum_t2num a
+   
+   [empty_enum_t2num_num2empty_enum_t]  Theorem
+      
+      ⊢ ∀r. r < 1 ⇔ empty_enum_t2num (num2empty_enum_t r) = r
+   
+   [empty_enum_t2num_thm]  Theorem
+      
+      ⊢ empty_enum_t2num EmptyEnumEmpty = 0
+   
+   [empty_enum_t_Axiom]  Theorem
+      
+      ⊢ ∀x0. ∃f. f EmptyEnumEmpty = x0
+   
+   [empty_enum_t_EQ_empty_enum_t]  Theorem
+      
+      ⊢ ∀a a'. a = a' ⇔ empty_enum_t2num a = empty_enum_t2num a'
+   
+   [empty_enum_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' v0.
+          M = M' ∧ (M' = EmptyEnumEmpty ⇒ v0 = v0') ⇒
+          (case M of EmptyEnumEmpty => v0) =
+          case M' of EmptyEnumEmpty => v0'
+   
+   [empty_enum_t_case_def]  Theorem
+      
+      ⊢ ∀v0. (case EmptyEnumEmpty of EmptyEnumEmpty => v0) = v0
+   
+   [empty_enum_t_case_eq]  Theorem
+      
+      ⊢ (case x of EmptyEnumEmpty => v0) = v ⇔ x = EmptyEnumEmpty ∧ v0 = v
+   
+   [empty_enum_t_induction]  Theorem
+      
+      ⊢ ∀P. P EmptyEnumEmpty ⇒ ∀a. P a
+   
+   [empty_enum_t_nchotomy]  Theorem
+      
+      ⊢ ∀a. a = EmptyEnumEmpty
+   
+   [enum_t2num_11]  Theorem
+      
+      ⊢ ∀a a'. enum_t2num a = enum_t2num a' ⇔ a = a'
+   
+   [enum_t2num_ONTO]  Theorem
+      
+      ⊢ ∀r. r < 2 ⇔ ∃a. r = enum_t2num a
+   
+   [enum_t2num_num2enum_t]  Theorem
+      
+      ⊢ ∀r. r < 2 ⇔ enum_t2num (num2enum_t r) = r
+   
+   [enum_t2num_thm]  Theorem
+      
+      ⊢ enum_t2num EnumVariant1 = 0 ∧ enum_t2num EnumVariant2 = 1
+   
+   [enum_t_Axiom]  Theorem
+      
+      ⊢ ∀x0 x1. ∃f. f EnumVariant1 = x0 ∧ f EnumVariant2 = x1
+   
+   [enum_t_EQ_enum_t]  Theorem
+      
+      ⊢ ∀a a'. a = a' ⇔ enum_t2num a = enum_t2num a'
+   
+   [enum_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' v0 v1.
+          M = M' ∧ (M' = EnumVariant1 ⇒ v0 = v0') ∧
+          (M' = EnumVariant2 ⇒ v1 = v1') ⇒
+          (case M of EnumVariant1 => v0 | EnumVariant2 => v1) =
+          case M' of EnumVariant1 => v0' | EnumVariant2 => v1'
+   
+   [enum_t_case_def]  Theorem
+      
+      ⊢ (∀v0 v1.
+           (case EnumVariant1 of EnumVariant1 => v0 | EnumVariant2 => v1) =
+           v0) ∧
+        ∀v0 v1.
+          (case EnumVariant2 of EnumVariant1 => v0 | EnumVariant2 => v1) =
+          v1
+   
+   [enum_t_case_eq]  Theorem
+      
+      ⊢ (case x of EnumVariant1 => v0 | EnumVariant2 => v1) = v ⇔
+        x = EnumVariant1 ∧ v0 = v ∨ x = EnumVariant2 ∧ v1 = v
+   
+   [enum_t_distinct]  Theorem
+      
+      ⊢ EnumVariant1 ≠ EnumVariant2
+   
+   [enum_t_induction]  Theorem
+      
+      ⊢ ∀P. P EnumVariant1 ∧ P EnumVariant2 ⇒ ∀a. P a
+   
+   [enum_t_nchotomy]  Theorem
+      
+      ⊢ ∀a. a = EnumVariant1 ∨ a = EnumVariant2
+   
+   [list_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'.
+          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [list_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+          fn ListNil = f1
+   
+   [list_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+          (M' = ListNil ⇒ v = v') ⇒
+          list_t_CASE M f v = list_t_CASE M' f' v'
+   
+   [list_t_case_eq]  Theorem
+      
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+   
+   [list_t_distinct]  Theorem
+      
+      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+   
+   [list_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+   
+   [list_t_nchotomy]  Theorem
+      
+      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+   
+   [node_elem_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'.
+          NodeElemCons a0 a1 = NodeElemCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [node_elem_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1 f2 f3. ∃fn0 fn1.
+          (∀a. fn0 (TreeLeaf a) = f0 a) ∧
+          (∀a0 a1 a2.
+             fn0 (TreeNode a0 a1 a2) = f1 a0 a1 a2 (fn1 a1) (fn0 a2)) ∧
+          (∀a0 a1. fn1 (NodeElemCons a0 a1) = f2 a0 a1 (fn0 a0) (fn1 a1)) ∧
+          fn1 NodeElemNil = f3
+   
+   [node_elem_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧ (∀a0 a1. M' = NodeElemCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+          (M' = NodeElemNil ⇒ v = v') ⇒
+          node_elem_t_CASE M f v = node_elem_t_CASE M' f' v'
+   
+   [node_elem_t_case_eq]  Theorem
+      
+      ⊢ node_elem_t_CASE x f v = v' ⇔
+        (∃t n. x = NodeElemCons t n ∧ f t n = v') ∨
+        x = NodeElemNil ∧ v = v'
+   
+   [node_elem_t_distinct]  Theorem
+      
+      ⊢ ∀a1 a0. NodeElemCons a0 a1 ≠ NodeElemNil
+   
+   [node_elem_t_induction]  Theorem
+      
+      ⊢ ∀P0 P1.
+          (∀t. P0 (TreeLeaf t)) ∧
+          (∀n t. P1 n ∧ P0 t ⇒ ∀t0. P0 (TreeNode t0 n t)) ∧
+          (∀t n. P0 t ∧ P1 n ⇒ P1 (NodeElemCons t n)) ∧ P1 NodeElemNil ⇒
+          (∀t. P0 t) ∧ ∀n. P1 n
+   
+   [node_elem_t_nchotomy]  Theorem
+      
+      ⊢ ∀nn. (∃t n. nn = NodeElemCons t n) ∨ nn = NodeElemNil
+   
+   [num2empty_enum_t_11]  Theorem
+      
+      ⊢ ∀r r'.
+          r < 1 ⇒
+          r' < 1 ⇒
+          (num2empty_enum_t r = num2empty_enum_t r' ⇔ r = r')
+   
+   [num2empty_enum_t_ONTO]  Theorem
+      
+      ⊢ ∀a. ∃r. a = num2empty_enum_t r ∧ r < 1
+   
+   [num2empty_enum_t_empty_enum_t2num]  Theorem
+      
+      ⊢ ∀a. num2empty_enum_t (empty_enum_t2num a) = a
+   
+   [num2empty_enum_t_thm]  Theorem
+      
+      ⊢ num2empty_enum_t 0 = EmptyEnumEmpty
+   
+   [num2enum_t_11]  Theorem
+      
+      ⊢ ∀r r'. r < 2 ⇒ r' < 2 ⇒ (num2enum_t r = num2enum_t r' ⇔ r = r')
+   
+   [num2enum_t_ONTO]  Theorem
+      
+      ⊢ ∀a. ∃r. a = num2enum_t r ∧ r < 2
+   
+   [num2enum_t_enum_t2num]  Theorem
+      
+      ⊢ ∀a. num2enum_t (enum_t2num a) = a
+   
+   [num2enum_t_thm]  Theorem
+      
+      ⊢ num2enum_t 0 = EnumVariant1 ∧ num2enum_t 1 = EnumVariant2
+   
+   [one_t_11]  Theorem
+      
+      ⊢ ∀a a'. OneOne a = OneOne a' ⇔ a = a'
+   
+   [one_t_Axiom]  Theorem
+      
+      ⊢ ∀f. ∃fn. ∀a. fn (OneOne a) = f a
+   
+   [one_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f.
+          M = M' ∧ (∀a. M' = OneOne a ⇒ f a = f' a) ⇒
+          one_t_CASE M f = one_t_CASE M' f'
+   
+   [one_t_case_eq]  Theorem
+      
+      ⊢ one_t_CASE x f = v ⇔ ∃t. x = OneOne t ∧ f t = v
+   
+   [one_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀t. P (OneOne t)) ⇒ ∀ $o. P $o
+   
+   [one_t_nchotomy]  Theorem
+      
+      ⊢ ∀oo. ∃t. oo = OneOne t
+   
+   [pair_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'. pair_t a0 a1 = pair_t a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [pair_t_Axiom]  Theorem
+      
+      ⊢ ∀f. ∃fn. ∀a0 a1. fn (pair_t a0 a1) = f a0 a1
+   
+   [pair_t_accessors]  Theorem
+      
+      ⊢ (∀t t0. (pair_t t t0).pair_x = t) ∧
+        ∀t t0. (pair_t t t0).pair_y = t0
+   
+   [pair_t_accfupds]  Theorem
+      
+      ⊢ (∀p f. (p with pair_y updated_by f).pair_x = p.pair_x) ∧
+        (∀p f. (p with pair_x updated_by f).pair_y = p.pair_y) ∧
+        (∀p f. (p with pair_x updated_by f).pair_x = f p.pair_x) ∧
+        ∀p f. (p with pair_y updated_by f).pair_y = f p.pair_y
+   
+   [pair_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f.
+          M = M' ∧ (∀a0 a1. M' = pair_t a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒
+          pair_t_CASE M f = pair_t_CASE M' f'
+   
+   [pair_t_case_eq]  Theorem
+      
+      ⊢ pair_t_CASE x f = v ⇔ ∃t t0. x = pair_t t t0 ∧ f t t0 = v
+   
+   [pair_t_component_equality]  Theorem
+      
+      ⊢ ∀p1 p2. p1 = p2 ⇔ p1.pair_x = p2.pair_x ∧ p1.pair_y = p2.pair_y
+   
+   [pair_t_fn_updates]  Theorem
+      
+      ⊢ (∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0) ∧
+        ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0)
+   
+   [pair_t_fupdcanon]  Theorem
+      
+      ⊢ ∀p g f.
+          p with <|pair_y updated_by f; pair_x updated_by g|> =
+          p with <|pair_x updated_by g; pair_y updated_by f|>
+   
+   [pair_t_fupdcanon_comp]  Theorem
+      
+      ⊢ (∀g f.
+           pair_y_fupd f ∘ pair_x_fupd g = pair_x_fupd g ∘ pair_y_fupd f) ∧
+        ∀h g f.
+          pair_y_fupd f ∘ pair_x_fupd g ∘ h =
+          pair_x_fupd g ∘ pair_y_fupd f ∘ h
+   
+   [pair_t_fupdfupds]  Theorem
+      
+      ⊢ (∀p g f.
+           p with <|pair_x updated_by f; pair_x updated_by g|> =
+           p with pair_x updated_by f ∘ g) ∧
+        ∀p g f.
+          p with <|pair_y updated_by f; pair_y updated_by g|> =
+          p with pair_y updated_by f ∘ g
+   
+   [pair_t_fupdfupds_comp]  Theorem
+      
+      ⊢ ((∀g f. pair_x_fupd f ∘ pair_x_fupd g = pair_x_fupd (f ∘ g)) ∧
+         ∀h g f.
+           pair_x_fupd f ∘ pair_x_fupd g ∘ h = pair_x_fupd (f ∘ g) ∘ h) ∧
+        (∀g f. pair_y_fupd f ∘ pair_y_fupd g = pair_y_fupd (f ∘ g)) ∧
+        ∀h g f. pair_y_fupd f ∘ pair_y_fupd g ∘ h = pair_y_fupd (f ∘ g) ∘ h
+   
+   [pair_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀t t0. P (pair_t t t0)) ⇒ ∀p. P p
+   
+   [pair_t_literal_11]  Theorem
+      
+      ⊢ ∀t01 t1 t02 t2.
+          <|pair_x := t01; pair_y := t1|> = <|pair_x := t02; pair_y := t2|> ⇔
+          t01 = t02 ∧ t1 = t2
+   
+   [pair_t_literal_nchotomy]  Theorem
+      
+      ⊢ ∀p. ∃t0 t. p = <|pair_x := t0; pair_y := t|>
+   
+   [pair_t_nchotomy]  Theorem
+      
+      ⊢ ∀pp. ∃t t0. pp = pair_t t t0
+   
+   [pair_t_updates_eq_literal]  Theorem
+      
+      ⊢ ∀p t0 t.
+          p with <|pair_x := t0; pair_y := t|> =
+          <|pair_x := t0; pair_y := t|>
+   
+   [struct_with_pair_t_11]  Theorem
+      
+      ⊢ ∀a a'. struct_with_pair_t a = struct_with_pair_t a' ⇔ a = a'
+   
+   [struct_with_pair_t_Axiom]  Theorem
+      
+      ⊢ ∀f. ∃fn. ∀a. fn (struct_with_pair_t a) = f a
+   
+   [struct_with_pair_t_accessors]  Theorem
+      
+      ⊢ ∀p. (struct_with_pair_t p).struct_with_pair_p = p
+   
+   [struct_with_pair_t_accfupds]  Theorem
+      
+      ⊢ ∀s f.
+          (s with struct_with_pair_p updated_by f).struct_with_pair_p =
+          f s.struct_with_pair_p
+   
+   [struct_with_pair_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f.
+          M = M' ∧ (∀a. M' = struct_with_pair_t a ⇒ f a = f' a) ⇒
+          struct_with_pair_t_CASE M f = struct_with_pair_t_CASE M' f'
+   
+   [struct_with_pair_t_case_eq]  Theorem
+      
+      ⊢ struct_with_pair_t_CASE x f = v ⇔
+        ∃p. x = struct_with_pair_t p ∧ f p = v
+   
+   [struct_with_pair_t_component_equality]  Theorem
+      
+      ⊢ ∀s1 s2. s1 = s2 ⇔ s1.struct_with_pair_p = s2.struct_with_pair_p
+   
+   [struct_with_pair_t_fn_updates]  Theorem
+      
+      ⊢ ∀f p.
+          struct_with_pair_t p with struct_with_pair_p updated_by f =
+          struct_with_pair_t (f p)
+   
+   [struct_with_pair_t_fupdfupds]  Theorem
+      
+      ⊢ ∀s g f.
+          s with
+          <|struct_with_pair_p updated_by f;
+            struct_with_pair_p updated_by g|> =
+          s with struct_with_pair_p updated_by f ∘ g
+   
+   [struct_with_pair_t_fupdfupds_comp]  Theorem
+      
+      ⊢ (∀g f.
+           struct_with_pair_p_fupd f ∘ struct_with_pair_p_fupd g =
+           struct_with_pair_p_fupd (f ∘ g)) ∧
+        ∀h g f.
+          struct_with_pair_p_fupd f ∘ struct_with_pair_p_fupd g ∘ h =
+          struct_with_pair_p_fupd (f ∘ g) ∘ h
+   
+   [struct_with_pair_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀p. P (struct_with_pair_t p)) ⇒ ∀s. P s
+   
+   [struct_with_pair_t_literal_11]  Theorem
+      
+      ⊢ ∀p1 p2.
+          <|struct_with_pair_p := p1|> = <|struct_with_pair_p := p2|> ⇔
+          p1 = p2
+   
+   [struct_with_pair_t_literal_nchotomy]  Theorem
+      
+      ⊢ ∀s. ∃p. s = <|struct_with_pair_p := p|>
+   
+   [struct_with_pair_t_nchotomy]  Theorem
+      
+      ⊢ ∀ss. ∃p. ss = struct_with_pair_t p
+   
+   [struct_with_pair_t_updates_eq_literal]  Theorem
+      
+      ⊢ ∀s p. s with struct_with_pair_p := p = <|struct_with_pair_p := p|>
+   
+   [struct_with_tuple_t_11]  Theorem
+      
+      ⊢ ∀a a'. struct_with_tuple_t a = struct_with_tuple_t a' ⇔ a = a'
+   
+   [struct_with_tuple_t_Axiom]  Theorem
+      
+      ⊢ ∀f. ∃fn. ∀a. fn (struct_with_tuple_t a) = f a
+   
+   [struct_with_tuple_t_accessors]  Theorem
+      
+      ⊢ ∀p. (struct_with_tuple_t p).struct_with_tuple_p = p
+   
+   [struct_with_tuple_t_accfupds]  Theorem
+      
+      ⊢ ∀s f.
+          (s with struct_with_tuple_p updated_by f).struct_with_tuple_p =
+          f s.struct_with_tuple_p
+   
+   [struct_with_tuple_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f.
+          M = M' ∧ (∀a. M' = struct_with_tuple_t a ⇒ f a = f' a) ⇒
+          struct_with_tuple_t_CASE M f = struct_with_tuple_t_CASE M' f'
+   
+   [struct_with_tuple_t_case_eq]  Theorem
+      
+      ⊢ struct_with_tuple_t_CASE x f = v ⇔
+        ∃p. x = struct_with_tuple_t p ∧ f p = v
+   
+   [struct_with_tuple_t_component_equality]  Theorem
+      
+      ⊢ ∀s1 s2. s1 = s2 ⇔ s1.struct_with_tuple_p = s2.struct_with_tuple_p
+   
+   [struct_with_tuple_t_fn_updates]  Theorem
+      
+      ⊢ ∀f p.
+          struct_with_tuple_t p with struct_with_tuple_p updated_by f =
+          struct_with_tuple_t (f p)
+   
+   [struct_with_tuple_t_fupdfupds]  Theorem
+      
+      ⊢ ∀s g f.
+          s with
+          <|struct_with_tuple_p updated_by f;
+            struct_with_tuple_p updated_by g|> =
+          s with struct_with_tuple_p updated_by f ∘ g
+   
+   [struct_with_tuple_t_fupdfupds_comp]  Theorem
+      
+      ⊢ (∀g f.
+           struct_with_tuple_p_fupd f ∘ struct_with_tuple_p_fupd g =
+           struct_with_tuple_p_fupd (f ∘ g)) ∧
+        ∀h g f.
+          struct_with_tuple_p_fupd f ∘ struct_with_tuple_p_fupd g ∘ h =
+          struct_with_tuple_p_fupd (f ∘ g) ∘ h
+   
+   [struct_with_tuple_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀p. P (struct_with_tuple_t p)) ⇒ ∀s. P s
+   
+   [struct_with_tuple_t_literal_11]  Theorem
+      
+      ⊢ ∀p1 p2.
+          <|struct_with_tuple_p := p1|> = <|struct_with_tuple_p := p2|> ⇔
+          p1 = p2
+   
+   [struct_with_tuple_t_literal_nchotomy]  Theorem
+      
+      ⊢ ∀s. ∃p. s = <|struct_with_tuple_p := p|>
+   
+   [struct_with_tuple_t_nchotomy]  Theorem
+      
+      ⊢ ∀ss. ∃p. ss = struct_with_tuple_t p
+   
+   [struct_with_tuple_t_updates_eq_literal]  Theorem
+      
+      ⊢ ∀s p.
+          s with struct_with_tuple_p := p = <|struct_with_tuple_p := p|>
+   
+   [sum_t_11]  Theorem
+      
+      ⊢ (∀a a'. SumLeft a = SumLeft a' ⇔ a = a') ∧
+        ∀a a'. SumRight a = SumRight a' ⇔ a = a'
+   
+   [sum_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a. fn (SumLeft a) = f0 a) ∧ ∀a. fn (SumRight a) = f1 a
+   
+   [sum_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1.
+          M = M' ∧ (∀a. M' = SumLeft a ⇒ f a = f' a) ∧
+          (∀a. M' = SumRight a ⇒ f1 a = f1' a) ⇒
+          sum_t_CASE M f f1 = sum_t_CASE M' f' f1'
+   
+   [sum_t_case_eq]  Theorem
+      
+      ⊢ sum_t_CASE x f f1 = v ⇔
+        (∃t. x = SumLeft t ∧ f t = v) ∨ ∃t. x = SumRight t ∧ f1 t = v
+   
+   [sum_t_distinct]  Theorem
+      
+      ⊢ ∀a' a. SumLeft a ≠ SumRight a'
+   
+   [sum_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀t. P (SumLeft t)) ∧ (∀t. P (SumRight t)) ⇒ ∀s. P s
+   
+   [sum_t_nchotomy]  Theorem
+      
+      ⊢ ∀ss. (∃t. ss = SumLeft t) ∨ ∃t. ss = SumRight t
+   
+   [tree_t_11]  Theorem
+      
+      ⊢ (∀a a'. TreeLeaf a = TreeLeaf a' ⇔ a = a') ∧
+        ∀a0 a1 a2 a0' a1' a2'.
+          TreeNode a0 a1 a2 = TreeNode a0' a1' a2' ⇔
+          a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
+   
+   [tree_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1 f2 f3. ∃fn0 fn1.
+          (∀a. fn0 (TreeLeaf a) = f0 a) ∧
+          (∀a0 a1 a2.
+             fn0 (TreeNode a0 a1 a2) = f1 a0 a1 a2 (fn1 a1) (fn0 a2)) ∧
+          (∀a0 a1. fn1 (NodeElemCons a0 a1) = f2 a0 a1 (fn0 a0) (fn1 a1)) ∧
+          fn1 NodeElemNil = f3
+   
+   [tree_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f f1.
+          M = M' ∧ (∀a. M' = TreeLeaf a ⇒ f a = f' a) ∧
+          (∀a0 a1 a2. M' = TreeNode a0 a1 a2 ⇒ f1 a0 a1 a2 = f1' a0 a1 a2) ⇒
+          tree_t_CASE M f f1 = tree_t_CASE M' f' f1'
+   
+   [tree_t_case_eq]  Theorem
+      
+      ⊢ tree_t_CASE x f f1 = v ⇔
+        (∃t. x = TreeLeaf t ∧ f t = v) ∨
+        ∃t0 n t. x = TreeNode t0 n t ∧ f1 t0 n t = v
+   
+   [tree_t_distinct]  Theorem
+      
+      ⊢ ∀a2 a1 a0 a. TreeLeaf a ≠ TreeNode a0 a1 a2
+   
+   [tree_t_induction]  Theorem
+      
+      ⊢ ∀P0 P1.
+          (∀t. P0 (TreeLeaf t)) ∧
+          (∀n t. P1 n ∧ P0 t ⇒ ∀t0. P0 (TreeNode t0 n t)) ∧
+          (∀t n. P0 t ∧ P1 n ⇒ P1 (NodeElemCons t n)) ∧ P1 NodeElemNil ⇒
+          (∀t. P0 t) ∧ ∀n. P1 n
+   
+   [tree_t_nchotomy]  Theorem
+      
+      ⊢ ∀tt. (∃t. tt = TreeLeaf t) ∨ ∃t0 n t. tt = TreeNode t0 n t
+   
+   
+*)
+end