Make more progress on primitivesScript.sml

2 files changed, 191 insertions, 209 deletions

diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 9da8505d..b1dd770b 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -185,85 +185,83 @@ val all_to_int_bounds_lemmas = [
    Note that for isize and usize, we write the lemmas in such a way that the
    proofs are easily automatable for constants.
  *)
-(* TODO: rename those *)
-val int_to_isize_id =
-  new_axiom ("int_to_isize_id",
-    “!n. (i16_min <= n \/ isize_min <= n) /\ (n <= i16_max \/ n <= isize_max) ==>
-         isize_to_int (int_to_isize n) = n”)
-
 (* TODO: remove the condition on u16_max, and make the massage tactic automatically use usize_bounds *)
-val int_to_usize_id =
-  new_axiom ("int_to_usize_id",
-    “!n. 0 <= n /\ (n <= u16_max \/ n <= usize_max) ==> usize_to_int (int_to_usize n) = n”)
+val isize_to_int_int_to_isize =
+  new_axiom ("isize_to_int_int_to_isize",
+    “!n. isize_min <= n /\ n <= isize_max ==> isize_to_int (int_to_isize n) = n”)
 
-val int_to_i8_id =
-  new_axiom ("int_to_i8_id",
+val i8_to_int_int_to_i8 =
+  new_axiom ("i8_to_int_int_to_i8",
     “!n. i8_min <= n /\ n <= i8_max ==> i8_to_int (int_to_i8 n) = n”)
 
-val int_to_i16_id =
-  new_axiom ("int_to_i16_id",
+val i16_to_int_int_to_i16 =
+  new_axiom ("i16_to_int_int_to_i16",
     “!n. i16_min <= n /\ n <= i16_max ==> i16_to_int (int_to_i16 n) = n”)
 
-val int_to_i32_id =
-  new_axiom ("int_to_i32_id",
+val i32_to_int_int_to_i32 =
+  new_axiom ("i32_to_int_int_to_i32",
     “!n. i32_min <= n /\ n <= i32_max ==> i32_to_int (int_to_i32 n) = n”)
 
-val int_to_i64_id =
-  new_axiom ("int_to_i64_id",
+val i64_to_int_int_to_i64 =
+  new_axiom ("i64_to_int_int_to_i64",
     “!n. i64_min <= n /\ n <= i64_max ==> i64_to_int (int_to_i64 n) = n”)
 
-val int_to_i128_id =
-  new_axiom ("int_to_i128_id",
+val i128_to_int_int_to_i128 =
+  new_axiom ("i128_to_int_int_to_i128",
     “!n. i128_min <= n /\ n <= i128_max ==> i128_to_int (int_to_i128 n) = n”)
 
-val int_to_u8_id =
-  new_axiom ("int_to_u8_id",
+val usize_to_int_int_to_usize =
+  new_axiom ("usize_to_int_int_to_usize",
+    “!n. 0 <= n /\ n <= usize_max ==> usize_to_int (int_to_usize n) = n”)
+
+val u8_to_int_int_to_u8 =
+  new_axiom ("u8_to_int_int_to_u8",
     “!n. 0 <= n /\ n <= u8_max ==> u8_to_int (int_to_u8 n) = n”)
 
-val int_to_u16_id =
-  new_axiom ("int_to_u16_id",
+val u16_to_int_int_to_u16 =
+  new_axiom ("u16_to_int_int_to_u16",
     “!n. 0 <= n /\ n <= u16_max ==> u16_to_int (int_to_u16 n) = n”)
 
-val int_to_u32_id =
-  new_axiom ("int_to_u32_id",
+val u32_to_int_int_to_u32 =
+  new_axiom ("u32_to_int_int_to_u32",
     “!n. 0 <= n /\ n <= u32_max ==> u32_to_int (int_to_u32 n) = n”)
 
-val int_to_u64_id =
-  new_axiom ("int_to_u64_id",
+val u64_to_int_int_to_u64 =
+  new_axiom ("u64_to_int_int_to_u64",
     “!n. 0 <= n /\ n <= u64_max ==> u64_to_int (int_to_u64 n) = n”)
 
-val int_to_u128_id =
-  new_axiom ("int_to_u128_id",
+val u128_to_int_int_to_u128 =
+  new_axiom ("u128_to_int_int_to_u128",
     “!n. 0 <= n /\ n <= u128_max ==> u128_to_int (int_to_u128 n) = n”)
 
 (* TODO: rename *)
 val all_conversion_id_lemmas = [
-  int_to_isize_id,
-  int_to_i8_id,
-  int_to_i16_id,
-  int_to_i32_id,
-  int_to_i64_id,
-  int_to_i128_id,
-  int_to_usize_id,
-  int_to_u8_id,
-  int_to_u16_id,
-  int_to_u32_id,
-  int_to_u64_id,
-  int_to_u128_id
+  isize_to_int_int_to_isize,
+  i8_to_int_int_to_i8,
+  i16_to_int_int_to_i16,
+  i32_to_int_int_to_i32,
+  i64_to_int_int_to_i64,
+  i128_to_int_int_to_i128,
+  usize_to_int_int_to_usize,
+  u8_to_int_int_to_u8,
+  u16_to_int_int_to_u16,
+  u32_to_int_int_to_u32,
+  u64_to_int_int_to_u64,
+  u128_to_int_int_to_u128
 ]
 
-val int_to_i8_i8_to_int = new_axiom ("int_to_i8_i8_to_int", “∀i. int_to_i8 (i8_to_int i) = i”)
-val int_to_i16_i16_to_int = new_axiom ("int_to_i16_i16_to_int", “∀i. int_to_i16 (i16_to_int i) = i”)
-val int_to_i32_i32_to_int = new_axiom ("int_to_i32_i32_to_int", “∀i. int_to_i32 (i32_to_int i) = i”)
-val int_to_i64_i64_to_int = new_axiom ("int_to_i64_i64_to_int", “∀i. int_to_i64 (i64_to_int i) = i”)
-val int_to_i128_i128_to_int = new_axiom ("int_to_i128_i128_to_int", “∀i. int_to_i128 (i128_to_int i) = i”)
+val int_to_i8_i8_to_int       = new_axiom ("int_to_i8_i8_to_int",       “∀i. int_to_i8 (i8_to_int i) = i”)
+val int_to_i16_i16_to_int     = new_axiom ("int_to_i16_i16_to_int",     “∀i. int_to_i16 (i16_to_int i) = i”)
+val int_to_i32_i32_to_int     = new_axiom ("int_to_i32_i32_to_int",     “∀i. int_to_i32 (i32_to_int i) = i”)
+val int_to_i64_i64_to_int     = new_axiom ("int_to_i64_i64_to_int",     “∀i. int_to_i64 (i64_to_int i) = i”)
+val int_to_i128_i128_to_int   = new_axiom ("int_to_i128_i128_to_int",   “∀i. int_to_i128 (i128_to_int i) = i”)
 val int_to_isize_isize_to_int = new_axiom ("int_to_isize_isize_to_int", “∀i. int_to_isize (isize_to_int i) = i”)
 
-val int_to_u8_u8_to_int = new_axiom ("int_to_u8_u8_to_int", “∀i. int_to_u8 (u8_to_int i) = i”)
-val int_to_u16_u16_to_int = new_axiom ("int_to_u16_u16_to_int", “∀i. int_to_u16 (u16_to_int i) = i”)
-val int_to_u32_u32_to_int = new_axiom ("int_to_u32_u32_to_int", “∀i. int_to_u32 (u32_to_int i) = i”)
-val int_to_u64_u64_to_int = new_axiom ("int_to_u64_u64_to_int", “∀i. int_to_u64 (u64_to_int i) = i”)
-val int_to_u128_u128_to_int = new_axiom ("int_to_u128_u128_to_int", “∀i. int_to_u128 (u128_to_int i) = i”)
+val int_to_u8_u8_to_int       = new_axiom ("int_to_u8_u8_to_int",       “∀i. int_to_u8 (u8_to_int i) = i”)
+val int_to_u16_u16_to_int     = new_axiom ("int_to_u16_u16_to_int",     “∀i. int_to_u16 (u16_to_int i) = i”)
+val int_to_u32_u32_to_int     = new_axiom ("int_to_u32_u32_to_int",     “∀i. int_to_u32 (u32_to_int i) = i”)
+val int_to_u64_u64_to_int     = new_axiom ("int_to_u64_u64_to_int",     “∀i. int_to_u64 (u64_to_int i) = i”)
+val int_to_u128_u128_to_int   = new_axiom ("int_to_u128_u128_to_int",   “∀i. int_to_u128 (u128_to_int i) = i”)
 val int_to_usize_usize_to_int = new_axiom ("int_to_usize_usize_to_int", “∀i. int_to_usize (usize_to_int i) = i”)
 
 (** Utilities to define the arithmetic operations *)
@@ -1266,14 +1264,11 @@ val vec_index_def = Define ‘
 (* TODO: use cooper_tac everywhere *)
 (* TODO: use pure_once_rewrite_tac everywhere *)
 
-(* TODO: injectivity lemmas for ..._to_int *)
+(*
 Theorem usize_to_int_inj:
   ∀i j. usize_to_int i = usize_to_int j ⇔ i = j
 Proof
-  rpt strip_tac >>
-  qspec_assume ‘i’ int_to_usize_usize_to_int >>
-  qspec_assume ‘j’ int_to_usize_usize_to_int >>
-  metis_tac []
+  metis_tac [int_to_usize_usize_to_int]
 QED
 
 Theorem usize_to_int_neq_inj:
@@ -1281,6 +1276,7 @@ Theorem usize_to_int_neq_inj:
 Proof
   metis_tac [usize_to_int_inj]
 QED
+*)
 
 Theorem int_of_num_neq_inj:
   ∀n m. &n ≠ &m ⇒ n ≠ m
@@ -1324,7 +1320,7 @@ Proof
   rw [] >> gvs [] >>
   fs [vec_len_def, vec_index_def] >>
   sg ‘usize_to_int (int_to_usize (&LENGTH (vec_to_list v))) = &LENGTH (vec_to_list v)’
-  >-(irule int_to_usize_id >> cooper_tac) >>
+  >-(irule usize_to_int_int_to_usize >> cooper_tac) >>
   fs [] >>
   qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_spec >> rfs [] >>
   sg ‘Num (usize_to_int i) < LENGTH (vec_to_list v)’ >-(
@@ -1342,7 +1338,7 @@ Proof
     irule int_of_num_neq_inj >>
     dep_pure_rewrite_tac [primitivesArithTheory.int_of_num] >>
     rw [usize_to_int_bounds] >>
-    metis_tac [usize_to_int_neq_inj]
+    metis_tac [int_to_usize_usize_to_int]
   ) >>
   (* TODO: automate *)
   pure_once_rewrite_tac [gsym INT_LT] >>
@@ -1350,8 +1346,6 @@ Proof
   qspec_assume ‘j’ usize_to_int_bounds >> fs []
 QED
 
-(* TODO: use lowercase everywhere for the theorem names *)
-
 
 (* Small experiment: trying to redefine common functions with integers instead of nums *)
 val index_def = Define ‘
@@ -1468,7 +1462,7 @@ Proof
   rw [] >> gvs [] >>
   fs [vec_len_def, vec_index_def] >>
   qspec_assume ‘i’ usize_to_int_bounds >>
-  sg_dep_rewrite_all_tac int_to_usize_id >- cooper_tac >> fs [] >>
+  sg_dep_rewrite_all_tac usize_to_int_int_to_usize >- cooper_tac >> fs [] >>
   sg_dep_rewrite_goal_tac index_update_diff >- cooper_tac >> fs [] >>
   rw [] >>
   irule index_update_same >> cooper_tac
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 66adac64..92f02af8 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -4,44 +4,44 @@ sig
   
   (*  Axioms  *)
     val i128_to_int_bounds : thm
+    val i128_to_int_int_to_i128 : thm
     val i16_to_int_bounds : thm
+    val i16_to_int_int_to_i16 : thm
     val i32_to_int_bounds : thm
+    val i32_to_int_int_to_i32 : thm
     val i64_to_int_bounds : thm
+    val i64_to_int_int_to_i64 : thm
     val i8_to_int_bounds : thm
+    val i8_to_int_int_to_i8 : thm
     val int_to_i128_i128_to_int : thm
-    val int_to_i128_id : thm
     val int_to_i16_i16_to_int : thm
-    val int_to_i16_id : thm
     val int_to_i32_i32_to_int : thm
-    val int_to_i32_id : thm
     val int_to_i64_i64_to_int : thm
-    val int_to_i64_id : thm
     val int_to_i8_i8_to_int : thm
-    val int_to_i8_id : thm
-    val int_to_isize_id : thm
     val int_to_isize_isize_to_int : thm
-    val int_to_u128_id : thm
     val int_to_u128_u128_to_int : thm
-    val int_to_u16_id : thm
     val int_to_u16_u16_to_int : thm
-    val int_to_u32_id : thm
     val int_to_u32_u32_to_int : thm
-    val int_to_u64_id : thm
     val int_to_u64_u64_to_int : thm
-    val int_to_u8_id : thm
     val int_to_u8_u8_to_int : thm
-    val int_to_usize_id : thm
     val int_to_usize_usize_to_int : thm
     val isize_bounds : thm
     val isize_to_int_bounds : thm
+    val isize_to_int_int_to_isize : thm
     val mk_vec_spec : thm
     val u128_to_int_bounds : thm
+    val u128_to_int_int_to_u128 : thm
     val u16_to_int_bounds : thm
+    val u16_to_int_int_to_u16 : thm
     val u32_to_int_bounds : thm
+    val u32_to_int_int_to_u32 : thm
     val u64_to_int_bounds : thm
+    val u64_to_int_int_to_u64 : thm
     val u8_to_int_bounds : thm
+    val u8_to_int_int_to_u8 : thm
     val usize_bounds : thm
     val usize_to_int_bounds : thm
+    val usize_to_int_int_to_usize : thm
     val vec_to_list_num_bounds : thm
   
   (*  Definitions  *)
@@ -245,8 +245,6 @@ sig
     val usize_mul_eq : thm
     val usize_rem_eq : thm
     val usize_sub_eq : thm
-    val usize_to_int_inj : thm
-    val usize_to_int_neq_inj : thm
     val vec_insert_back_spec : thm
     val vec_len_spec : thm
     val vec_to_list_int_bounds : thm
@@ -327,66 +325,65 @@ sig
       [oracles: ] [axioms: int_to_i8_i8_to_int] []
       ⊢ ∀i. int_to_i8 (i8_to_int i) = i
    
-   [int_to_u128_id]  Axiom
+   [u128_to_int_int_to_u128]  Axiom
       
-      [oracles: ] [axioms: int_to_u128_id] []
+      [oracles: ] [axioms: u128_to_int_int_to_u128] []
       ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
    
-   [int_to_u64_id]  Axiom
+   [u64_to_int_int_to_u64]  Axiom
       
-      [oracles: ] [axioms: int_to_u64_id] []
+      [oracles: ] [axioms: u64_to_int_int_to_u64] []
       ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
    
-   [int_to_u32_id]  Axiom
+   [u32_to_int_int_to_u32]  Axiom
       
-      [oracles: ] [axioms: int_to_u32_id] []
+      [oracles: ] [axioms: u32_to_int_int_to_u32] []
       ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
    
-   [int_to_u16_id]  Axiom
+   [u16_to_int_int_to_u16]  Axiom
       
-      [oracles: ] [axioms: int_to_u16_id] []
+      [oracles: ] [axioms: u16_to_int_int_to_u16] []
       ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
    
-   [int_to_u8_id]  Axiom
+   [u8_to_int_int_to_u8]  Axiom
       
-      [oracles: ] [axioms: int_to_u8_id] []
+      [oracles: ] [axioms: u8_to_int_int_to_u8] []
       ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
    
-   [int_to_i128_id]  Axiom
+   [usize_to_int_int_to_usize]  Axiom
       
-      [oracles: ] [axioms: int_to_i128_id] []
+      [oracles: ] [axioms: usize_to_int_int_to_usize] []
+      ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n
+   
+   [i128_to_int_int_to_i128]  Axiom
+      
+      [oracles: ] [axioms: i128_to_int_int_to_i128] []
       ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
    
-   [int_to_i64_id]  Axiom
+   [i64_to_int_int_to_i64]  Axiom
       
-      [oracles: ] [axioms: int_to_i64_id] []
+      [oracles: ] [axioms: i64_to_int_int_to_i64] []
       ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
    
-   [int_to_i32_id]  Axiom
+   [i32_to_int_int_to_i32]  Axiom
       
-      [oracles: ] [axioms: int_to_i32_id] []
+      [oracles: ] [axioms: i32_to_int_int_to_i32] []
       ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
    
-   [int_to_i16_id]  Axiom
+   [i16_to_int_int_to_i16]  Axiom
       
-      [oracles: ] [axioms: int_to_i16_id] []
+      [oracles: ] [axioms: i16_to_int_int_to_i16] []
       ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
    
-   [int_to_i8_id]  Axiom
+   [i8_to_int_int_to_i8]  Axiom
       
-      [oracles: ] [axioms: int_to_i8_id] []
+      [oracles: ] [axioms: i8_to_int_int_to_i8] []
       ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
    
-   [int_to_usize_id]  Axiom
+   [isize_to_int_int_to_isize]  Axiom
       
-      [oracles: ] [axioms: int_to_usize_id] []
-      ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒
-            usize_to_int (int_to_usize n) = n
-   
-   [int_to_isize_id]  Axiom
-      
-      [oracles: ] [axioms: int_to_isize_id] []
-      ⊢ ∀n. (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max) ⇒
+      [oracles: ] [axioms: isize_to_int_int_to_isize] []
+      ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒
             isize_to_int (int_to_isize n) = n
    
    [u128_to_int_bounds]  Axiom
@@ -1083,7 +1080,7 @@ sig
    [i128_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
+      [axioms: isize_bounds, i128_to_int_int_to_i128, usize_bounds] []
       ⊢ ∀x y.
           i128_min ≤ i128_to_int x + i128_to_int y ⇒
           i128_to_int x + i128_to_int y ≤ i128_max ⇒
@@ -1093,7 +1090,7 @@ sig
    [i128_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
+      [axioms: isize_bounds, i128_to_int_int_to_i128, usize_bounds] []
       ⊢ ∀x y.
           i128_to_int y ≠ 0 ⇒
           i128_min ≤ i128_to_int x / i128_to_int y ⇒
@@ -1104,7 +1101,7 @@ sig
    [i128_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
+      [axioms: isize_bounds, i128_to_int_int_to_i128, usize_bounds] []
       ⊢ ∀x y.
           i128_min ≤ i128_to_int x * i128_to_int y ⇒
           i128_to_int x * i128_to_int y ≤ i128_max ⇒
@@ -1114,7 +1111,7 @@ sig
    [i128_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i128_id, i128_to_int_bounds,
+      [axioms: isize_bounds, i128_to_int_int_to_i128, i128_to_int_bounds,
        usize_bounds] []
       ⊢ ∀x y.
           i128_to_int y ≠ 0 ⇒
@@ -1126,7 +1123,7 @@ sig
    [i128_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i128_id, usize_bounds] []
+      [axioms: isize_bounds, i128_to_int_int_to_i128, usize_bounds] []
       ⊢ ∀x y.
           i128_min ≤ i128_to_int x − i128_to_int y ⇒
           i128_to_int x − i128_to_int y ≤ i128_max ⇒
@@ -1136,7 +1133,7 @@ sig
    [i16_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
+      [axioms: isize_bounds, i16_to_int_int_to_i16, usize_bounds] []
       ⊢ ∀x y.
           i16_min ≤ i16_to_int x + i16_to_int y ⇒
           i16_to_int x + i16_to_int y ≤ i16_max ⇒
@@ -1146,7 +1143,7 @@ sig
    [i16_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
+      [axioms: isize_bounds, i16_to_int_int_to_i16, usize_bounds] []
       ⊢ ∀x y.
           i16_to_int y ≠ 0 ⇒
           i16_min ≤ i16_to_int x / i16_to_int y ⇒
@@ -1157,7 +1154,7 @@ sig
    [i16_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
+      [axioms: isize_bounds, i16_to_int_int_to_i16, usize_bounds] []
       ⊢ ∀x y.
           i16_min ≤ i16_to_int x * i16_to_int y ⇒
           i16_to_int x * i16_to_int y ≤ i16_max ⇒
@@ -1167,8 +1164,8 @@ sig
    [i16_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i16_id, i16_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, i16_to_int_int_to_i16, i16_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           i16_to_int y ≠ 0 ⇒
           i16_min ≤ int_rem (i16_to_int x) (i16_to_int y) ⇒
@@ -1179,7 +1176,7 @@ sig
    [i16_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i16_id, usize_bounds] []
+      [axioms: isize_bounds, i16_to_int_int_to_i16, usize_bounds] []
       ⊢ ∀x y.
           i16_min ≤ i16_to_int x − i16_to_int y ⇒
           i16_to_int x − i16_to_int y ≤ i16_max ⇒
@@ -1189,7 +1186,7 @@ sig
    [i32_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
+      [axioms: isize_bounds, i32_to_int_int_to_i32, usize_bounds] []
       ⊢ ∀x y.
           i32_min ≤ i32_to_int x + i32_to_int y ⇒
           i32_to_int x + i32_to_int y ≤ i32_max ⇒
@@ -1199,7 +1196,7 @@ sig
    [i32_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
+      [axioms: isize_bounds, i32_to_int_int_to_i32, usize_bounds] []
       ⊢ ∀x y.
           i32_to_int y ≠ 0 ⇒
           i32_min ≤ i32_to_int x / i32_to_int y ⇒
@@ -1210,7 +1207,7 @@ sig
    [i32_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
+      [axioms: isize_bounds, i32_to_int_int_to_i32, usize_bounds] []
       ⊢ ∀x y.
           i32_min ≤ i32_to_int x * i32_to_int y ⇒
           i32_to_int x * i32_to_int y ≤ i32_max ⇒
@@ -1220,8 +1217,8 @@ sig
    [i32_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i32_id, i32_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, i32_to_int_int_to_i32, i32_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           i32_to_int y ≠ 0 ⇒
           i32_min ≤ int_rem (i32_to_int x) (i32_to_int y) ⇒
@@ -1232,7 +1229,7 @@ sig
    [i32_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i32_id, usize_bounds] []
+      [axioms: isize_bounds, i32_to_int_int_to_i32, usize_bounds] []
       ⊢ ∀x y.
           i32_min ≤ i32_to_int x − i32_to_int y ⇒
           i32_to_int x − i32_to_int y ≤ i32_max ⇒
@@ -1242,7 +1239,7 @@ sig
    [i64_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
+      [axioms: isize_bounds, i64_to_int_int_to_i64, usize_bounds] []
       ⊢ ∀x y.
           i64_min ≤ i64_to_int x + i64_to_int y ⇒
           i64_to_int x + i64_to_int y ≤ i64_max ⇒
@@ -1252,7 +1249,7 @@ sig
    [i64_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
+      [axioms: isize_bounds, i64_to_int_int_to_i64, usize_bounds] []
       ⊢ ∀x y.
           i64_to_int y ≠ 0 ⇒
           i64_min ≤ i64_to_int x / i64_to_int y ⇒
@@ -1263,7 +1260,7 @@ sig
    [i64_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
+      [axioms: isize_bounds, i64_to_int_int_to_i64, usize_bounds] []
       ⊢ ∀x y.
           i64_min ≤ i64_to_int x * i64_to_int y ⇒
           i64_to_int x * i64_to_int y ≤ i64_max ⇒
@@ -1273,8 +1270,8 @@ sig
    [i64_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i64_id, i64_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, i64_to_int_int_to_i64, i64_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           i64_to_int y ≠ 0 ⇒
           i64_min ≤ int_rem (i64_to_int x) (i64_to_int y) ⇒
@@ -1285,7 +1282,7 @@ sig
    [i64_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i64_id, usize_bounds] []
+      [axioms: isize_bounds, i64_to_int_int_to_i64, usize_bounds] []
       ⊢ ∀x y.
           i64_min ≤ i64_to_int x − i64_to_int y ⇒
           i64_to_int x − i64_to_int y ≤ i64_max ⇒
@@ -1295,7 +1292,7 @@ sig
    [i8_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
+      [axioms: isize_bounds, i8_to_int_int_to_i8, usize_bounds] []
       ⊢ ∀x y.
           i8_min ≤ i8_to_int x + i8_to_int y ⇒
           i8_to_int x + i8_to_int y ≤ i8_max ⇒
@@ -1305,7 +1302,7 @@ sig
    [i8_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
+      [axioms: isize_bounds, i8_to_int_int_to_i8, usize_bounds] []
       ⊢ ∀x y.
           i8_to_int y ≠ 0 ⇒
           i8_min ≤ i8_to_int x / i8_to_int y ⇒
@@ -1316,7 +1313,7 @@ sig
    [i8_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
+      [axioms: isize_bounds, i8_to_int_int_to_i8, usize_bounds] []
       ⊢ ∀x y.
           i8_min ≤ i8_to_int x * i8_to_int y ⇒
           i8_to_int x * i8_to_int y ≤ i8_max ⇒
@@ -1326,8 +1323,8 @@ sig
    [i8_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i8_id, i8_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, i8_to_int_int_to_i8, i8_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           i8_to_int y ≠ 0 ⇒
           i8_min ≤ int_rem (i8_to_int x) (i8_to_int y) ⇒
@@ -1338,7 +1335,7 @@ sig
    [i8_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_i8_id, usize_bounds] []
+      [axioms: isize_bounds, i8_to_int_int_to_i8, usize_bounds] []
       ⊢ ∀x y.
           i8_min ≤ i8_to_int x − i8_to_int y ⇒
           i8_to_int x − i8_to_int y ≤ i8_max ⇒
@@ -1365,8 +1362,8 @@ sig
    [isize_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, isize_to_int_int_to_isize,
+       isize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           i16_min ≤ isize_to_int x + isize_to_int y ∨
           isize_min ≤ isize_to_int x + isize_to_int y ⇒
@@ -1378,8 +1375,8 @@ sig
    [isize_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, isize_to_int_int_to_isize,
+       isize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           isize_to_int y ≠ 0 ⇒
           i16_min ≤ isize_to_int x / isize_to_int y ∨
@@ -1392,8 +1389,8 @@ sig
    [isize_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, isize_to_int_int_to_isize,
+       isize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           i16_min ≤ isize_to_int x * isize_to_int y ∨
           isize_min ≤ isize_to_int x * isize_to_int y ⇒
@@ -1405,8 +1402,8 @@ sig
    [isize_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, isize_to_int_int_to_isize,
+       isize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           isize_to_int y ≠ 0 ⇒
           i16_min ≤ int_rem (isize_to_int x) (isize_to_int y) ∨
@@ -1419,8 +1416,8 @@ sig
    [isize_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_isize_id, isize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, isize_to_int_int_to_isize,
+       isize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           i16_min ≤ isize_to_int x − isize_to_int y ∨
           isize_min ≤ isize_to_int x − isize_to_int y ⇒
@@ -1485,7 +1482,7 @@ sig
    [u128_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+      [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
        usize_bounds] []
       ⊢ ∀x y.
           u128_to_int x + u128_to_int y ≤ u128_max ⇒
@@ -1495,7 +1492,7 @@ sig
    [u128_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+      [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
        usize_bounds] []
       ⊢ ∀x y.
           u128_to_int y ≠ 0 ⇒
@@ -1505,7 +1502,7 @@ sig
    [u128_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+      [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
        usize_bounds] []
       ⊢ ∀x y.
           u128_to_int x * u128_to_int y ≤ u128_max ⇒
@@ -1515,7 +1512,7 @@ sig
    [u128_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+      [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
        usize_bounds] []
       ⊢ ∀x y.
           u128_to_int y ≠ 0 ⇒
@@ -1525,7 +1522,7 @@ sig
    [u128_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u128_id, u128_to_int_bounds,
+      [axioms: isize_bounds, u128_to_int_int_to_u128, u128_to_int_bounds,
        usize_bounds] []
       ⊢ ∀x y.
           0 ≤ u128_to_int x − u128_to_int y ⇒
@@ -1535,8 +1532,8 @@ sig
    [u16_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u16_to_int x + u16_to_int y ≤ u16_max ⇒
           ∃z. u16_add x y = Return z ∧
@@ -1545,8 +1542,8 @@ sig
    [u16_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u16_to_int y ≠ 0 ⇒
           ∃z. u16_div x y = Return z ∧
@@ -1555,8 +1552,8 @@ sig
    [u16_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u16_to_int x * u16_to_int y ≤ u16_max ⇒
           ∃z. u16_mul x y = Return z ∧
@@ -1565,8 +1562,8 @@ sig
    [u16_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u16_to_int y ≠ 0 ⇒
           ∃z. u16_rem x y = Return z ∧
@@ -1575,8 +1572,8 @@ sig
    [u16_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u16_id, u16_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u16_to_int_int_to_u16, u16_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           0 ≤ u16_to_int x − u16_to_int y ⇒
           ∃z. u16_sub x y = Return z ∧
@@ -1585,8 +1582,8 @@ sig
    [u32_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u32_to_int x + u32_to_int y ≤ u32_max ⇒
           ∃z. u32_add x y = Return z ∧
@@ -1595,8 +1592,8 @@ sig
    [u32_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u32_to_int y ≠ 0 ⇒
           ∃z. u32_div x y = Return z ∧
@@ -1605,8 +1602,8 @@ sig
    [u32_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u32_to_int x * u32_to_int y ≤ u32_max ⇒
           ∃z. u32_mul x y = Return z ∧
@@ -1615,8 +1612,8 @@ sig
    [u32_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u32_to_int y ≠ 0 ⇒
           ∃z. u32_rem x y = Return z ∧
@@ -1625,8 +1622,8 @@ sig
    [u32_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u32_id, u32_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u32_to_int_int_to_u32, u32_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           0 ≤ u32_to_int x − u32_to_int y ⇒
           ∃z. u32_sub x y = Return z ∧
@@ -1635,8 +1632,8 @@ sig
    [u64_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u64_to_int x + u64_to_int y ≤ u64_max ⇒
           ∃z. u64_add x y = Return z ∧
@@ -1645,8 +1642,8 @@ sig
    [u64_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u64_to_int y ≠ 0 ⇒
           ∃z. u64_div x y = Return z ∧
@@ -1655,8 +1652,8 @@ sig
    [u64_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u64_to_int x * u64_to_int y ≤ u64_max ⇒
           ∃z. u64_mul x y = Return z ∧
@@ -1665,8 +1662,8 @@ sig
    [u64_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u64_to_int y ≠ 0 ⇒
           ∃z. u64_rem x y = Return z ∧
@@ -1675,8 +1672,8 @@ sig
    [u64_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u64_id, u64_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u64_to_int_int_to_u64, u64_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           0 ≤ u64_to_int x − u64_to_int y ⇒
           ∃z. u64_sub x y = Return z ∧
@@ -1685,8 +1682,8 @@ sig
    [u8_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u8_to_int x + u8_to_int y ≤ u8_max ⇒
           ∃z. u8_add x y = Return z ∧
@@ -1695,8 +1692,8 @@ sig
    [u8_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u8_to_int y ≠ 0 ⇒
           ∃z. u8_div x y = Return z ∧
@@ -1705,8 +1702,8 @@ sig
    [u8_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u8_to_int x * u8_to_int y ≤ u8_max ⇒
           ∃z. u8_mul x y = Return z ∧
@@ -1715,8 +1712,8 @@ sig
    [u8_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           u8_to_int y ≠ 0 ⇒
           ∃z. u8_rem x y = Return z ∧
@@ -1725,8 +1722,8 @@ sig
    [u8_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_u8_id, u8_to_int_bounds, usize_bounds]
-      []
+      [axioms: isize_bounds, u8_to_int_int_to_u8, u8_to_int_bounds,
+       usize_bounds] []
       ⊢ ∀x y.
           0 ≤ u8_to_int x − u8_to_int y ⇒
           ∃z. u8_sub x y = Return z ∧
@@ -1753,8 +1750,8 @@ sig
    [usize_add_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, usize_to_int_int_to_usize,
+       usize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           usize_to_int x + usize_to_int y ≤ u16_max ∨
           usize_to_int x + usize_to_int y ≤ usize_max ⇒
@@ -1764,8 +1761,8 @@ sig
    [usize_div_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, usize_to_int_int_to_usize,
+       usize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           usize_to_int y ≠ 0 ⇒
           ∃z. usize_div x y = Return z ∧
@@ -1774,8 +1771,8 @@ sig
    [usize_mul_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, usize_to_int_int_to_usize,
+       usize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           usize_to_int x * usize_to_int y ≤ u16_max ∨
           usize_to_int x * usize_to_int y ≤ usize_max ⇒
@@ -1785,8 +1782,8 @@ sig
    [usize_rem_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, usize_to_int_int_to_usize,
+       usize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           usize_to_int y ≠ 0 ⇒
           ∃z. usize_rem x y = Return z ∧
@@ -1795,27 +1792,18 @@ sig
    [usize_sub_eq]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: isize_bounds, int_to_usize_id, usize_to_int_bounds,
-       usize_bounds] []
+      [axioms: isize_bounds, usize_to_int_int_to_usize,
+       usize_to_int_bounds, usize_bounds] []
       ⊢ ∀x y.
           0 ≤ usize_to_int x − usize_to_int y ⇒
           ∃z. usize_sub x y = Return z ∧
               usize_to_int z = usize_to_int x − usize_to_int y
    
-   [usize_to_int_inj]  Theorem
-      
-      [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
-      ⊢ ∀i j. usize_to_int i = usize_to_int j ⇔ i = j
-   
-   [usize_to_int_neq_inj]  Theorem
-      
-      [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
-      ⊢ ∀i j. i ≠ j ⇒ usize_to_int i ≠ usize_to_int j
-   
    [vec_insert_back_spec]  Theorem
       
       [oracles: DISK_THM, cheat]
-      [axioms: usize_to_int_bounds, int_to_usize_id, mk_vec_spec] []
+      [axioms: usize_to_int_bounds, usize_to_int_int_to_usize, mk_vec_spec]
+      []
       ⊢ ∀v i x.
           usize_to_int i < usize_to_int (vec_len v) ⇒
           ∃nv.