diff --git a/code/gf128/Hacl.Spec.GF128.PolyLemmas.fst b/code/gf128/Hacl.Spec.GF128.PolyLemmas.fst
index 9dcd0f8801..e1ee3ab848 100644
--- a/code/gf128/Hacl.Spec.GF128.PolyLemmas.fst
+++ b/code/gf128/Hacl.Spec.GF128.PolyLemmas.fst
@@ -198,13 +198,91 @@ let logxor_disjoint #n a b m =
   assert (from_vec #m (slice #bool #n (to_vec b) (n - m) n) == b)
 #pop-options
 
+open Lib.ByteSequence
+
+val vec_cast_uint128: v1:vec_t U128 1 -> Lemma
+  (vec_v (cast U64 2 v1) == create2
+     (to_u64 ((index (vec_v v1) 0) >>. 64ul))
+     (to_u64 (index (vec_v v1) 0)))
+
+let vec_cast_uint128 v1 =
+  let v1_v = vec_v v1 in
+  assert (vec_v (cast U64 2 v1) == uints_from_bytes_be #U64 #SEC #2 (uints_to_bytes_be v1_v));
+  nat_from_intseq_be_lemma0 v1_v;
+  assert (nat_from_intseq_be v1_v == v (index v1_v 0));
+  lemma_nat_from_to_intseq_be_preserves_value 1 v1_v;
+  assert (nat_to_intseq_be 1 (nat_from_intseq_be v1_v) == v1_v);
+  uints_to_bytes_be_nat_lemma #U128 #SEC 1 (nat_from_intseq_be v1_v);
+  assert (uints_to_bytes_be v1_v == nat_to_intseq_be #U8 #SEC 16 (v (index v1_v 0)));
+  lemma_nat_from_to_intseq_be_preserves_value 2 (uints_from_bytes_be #U64 #SEC #2 (uints_to_bytes_be v1_v));
+  assert (nat_to_intseq_be 2 (nat_from_intseq_be #U64 #SEC (uints_from_bytes_be #U64 #SEC #2 (uints_to_bytes_be v1_v))) ==
+    uints_from_bytes_be #U64 #SEC #2 (uints_to_bytes_be v1_v));
+  uints_from_bytes_be_nat_lemma #U64 #SEC #2 (uints_to_bytes_be v1_v);
+  assert (nat_to_intseq_be 2 (nat_from_bytes_be (uints_to_bytes_be v1_v)) ==
+    uints_from_bytes_be #U64 #SEC #2 (uints_to_bytes_be v1_v));
+  assert (vec_v (cast U64 2 v1) == nat_to_intseq_be 2 (nat_from_bytes_be (nat_to_intseq_be #U8 #SEC 16 (v (index v1_v 0)))));
+  lemma_nat_to_from_bytes_be_preserves_value #SEC (nat_to_intseq_be #U8 #SEC 16 (v (index v1_v 0))) 16 (v (index v1_v 0));
+  assert (vec_v (cast U64 2 v1) == nat_to_intseq_be 2 (v (index v1_v 0)));
+  index_nat_to_intseq_be #U64 #SEC 2 (v (index v1_v 0)) 0;
+  assert (Seq.index (nat_to_intseq_be 2 (v (index v1_v 0))) 1 ==
+    uint #U64 #SEC ((v (index v1_v 0)) / pow2 0 % pow2 64));
+  assert ((v (index v1_v 0)) / pow2 0 % pow2 64 == v (index v1_v 0) % pow2 64);
+  index_nat_to_intseq_be #U64 #SEC 2 (v (index v1_v 0)) 1;
+  assert (Seq.index (nat_to_intseq_be 2 (v (index v1_v 0))) 0 ==
+    uint #U64 #SEC ((v (index v1_v 0)) / pow2 64 % pow2 64));
+  assert ((v (index v1_v 0)) / pow2 64 % pow2 64 == v (index v1_v 0) / pow2 64);
+  assert (v (index v1_v 0) / pow2 64 == v ((index v1_v 0) >>. 64ul));
+  eq_intro (nat_to_intseq_be #U64 #SEC 2 (v (index v1_v 0)))
+    (create2 (uint #U64 #SEC (v ((index v1_v 0) >>. 64ul))) (uint #U64 #SEC (v (index v1_v 0) % pow2 64)))
+
+val vec_cast_2_uint64: v1:vec_t U64 2 -> Lemma
+  (vec_v (cast U128 1 v1) == create 1
+    (to_u128 (index (vec_v v1) 1) +! ((to_u128 (index (vec_v v1) 0)) <<. 64ul)))
+
+#push-options "--z3rlimit 20"
+let vec_cast_2_uint64 v1 =
+  let v1_v = vec_v v1 in
+  assert (vec_v (cast U128 1 v1) == uints_from_bytes_be #U128 #SEC #1 (uints_to_bytes_be v1_v));
+  lemma_nat_from_to_intseq_be_preserves_value 2 v1_v;
+  assert (nat_to_intseq_be 2 (nat_from_intseq_be v1_v) == v1_v);
+  uints_to_bytes_be_nat_lemma #U64 #SEC 2 (nat_from_intseq_be v1_v);
+  assert (nat_to_bytes_be 16 (nat_from_intseq_be v1_v) == uints_to_bytes_be v1_v);
+  lemma_nat_from_to_intseq_be_preserves_value 1 (uints_from_bytes_be #U128 #SEC #1 (uints_to_bytes_be v1_v));
+  assert (nat_to_intseq_be 1 (nat_from_intseq_be (uints_from_bytes_be #U128 #SEC #1 (uints_to_bytes_be v1_v))) ==
+    uints_from_bytes_be #U128 #SEC #1 (uints_to_bytes_be v1_v));
+  uints_from_bytes_be_nat_lemma #U128 #SEC #1 (uints_to_bytes_be v1_v);
+  assert (nat_to_intseq_be 1 (nat_from_bytes_be (uints_to_bytes_be v1_v)) == uints_from_bytes_be #U128 #SEC #1 (uints_to_bytes_be v1_v));
+  assert (nat_to_intseq_be 1 (nat_from_bytes_be (nat_to_bytes_be #SEC 16 (nat_from_intseq_be v1_v))) ==
+    uints_from_bytes_be #U128 #SEC #1 (uints_to_bytes_be v1_v));
+  lemma_nat_to_from_bytes_be_preserves_value #SEC (nat_to_bytes_be #SEC 16 (nat_from_intseq_be v1_v)) 16 (nat_from_intseq_be v1_v);
+  assert (nat_to_intseq_be 1 (nat_from_intseq_be v1_v) == vec_v (cast U128 1 v1));
+
+  nat_from_intseq_be_slice_lemma #U64 #SEC #2 v1_v 1;
+  assert (nat_from_intseq_be v1_v == nat_from_intseq_be (slice v1_v 1 2) + pow2 64 * nat_from_intseq_be (slice v1_v 0 1));
+  nat_from_intseq_be_lemma0 #U64 #SEC (slice v1_v 1 2);
+  assert (nat_from_intseq_be (slice v1_v 1 2) == v (index v1_v 1));
+  nat_from_intseq_be_lemma0 #U64 #SEC (slice v1_v 0 1);
+  assert (nat_from_intseq_be (slice v1_v 0 1) == v (index v1_v 0));
+
+  assert (pow2 64 * v (index v1_v 0) == v ((to_u128 (index (vec_v v1) 0)) <<. 64ul));
+  assert (v (index v1_v 1) == v (to_u128 (index (vec_v v1) 1)));
+  assert (v (to_u128 (index (vec_v v1) 1)) + v ((to_u128 (index (vec_v v1) 0)) <<. 64ul) ==
+    v ((to_u128 (index (vec_v v1) 1)) +! ((to_u128 (index (vec_v v1) 0)) <<. 64ul)));
+
+  index_nat_to_intseq_be #U128 #SEC 1 (nat_from_intseq_be v1_v) 0;
+  assert (Seq.index (nat_to_intseq_be 1 (nat_from_intseq_be v1_v)) 0 ==
+    uint #U128 #SEC (nat_from_intseq_be v1_v));
+  eq_intro (nat_to_intseq_be 1 (nat_from_intseq_be v1_v))
+    (create 1 (uint #U128 #SEC (v ((to_u128 (index (vec_v v1) 1)) +! ((to_u128 (index (vec_v v1) 0)) <<. 64ul)))))
+#pop-options
+
 #push-options "--z3rlimit 150 --max_fuel 1"
 let lemma_vec128_shift_left_64 p s =
   vec_cast_uint128 p;
   vec_cast_2_uint64 (vec_shift_left (V.cast U64 2 p) s);
   eq_elim (map (shift_left_i s) (vec_v (V.cast U64 2 p))) (create2
-    (shift_left_i s (to_u64 (index (vec_v p) 0)))
     (shift_left_i s (to_u64 (T.shift_right (index (vec_v p) 0) 64ul)))
+    (shift_left_i s (to_u64 (index (vec_v p) 0)))
   );
   reveal_vec_v_1 p;
   reveal_vec_v_1 (V.cast U128 1 (vec_shift_left (V.cast U64 2 p) s));
@@ -216,8 +294,8 @@ let lemma_vec128_shift_left_64 p s =
   let p0 = (((to_uint 128 a) % pow2 64) * pow2 (v s)) % pow2 64 in
   let p1 = ((((to_uint 128 a) / pow2 64) % pow2 64) * pow2 (v s)) % pow2 64 in
   let t = T.add
-          (T.shift_left (to_u128 (shift_left_i s (to_u64 (T.shift_right #U128 #SEC p 64ul)))) 64ul)
-          (to_u128 (shift_left_i s (to_u64 #U128 #SEC p))) in
+          (to_u128 (shift_left_i s (to_u64 #U128 #SEC p)))
+          (T.shift_left (to_u128 (shift_left_i s (to_u64 (T.shift_right #U128 #SEC p 64ul)))) 64ul) in
   assert (t == V.cast U128 1 (vec_shift_left (V.cast U64 2 p) s));
   reveal_vec_v_1 #U128 t;
   assert (of_vec128 t == of_uint 128 (p1 * pow2 64 + p0));
@@ -260,8 +338,8 @@ let lemma_vec128_shift_right_64 p s =
   vec_cast_uint128 p;
   vec_cast_2_uint64 (vec_shift_right (V.cast U64 2 p) s);
   eq_elim (map (shift_right_i s) (vec_v (V.cast U64 2 p))) (create2
-    (shift_right_i s (to_u64 (index (vec_v p) 0)))
     (shift_right_i s (to_u64 (T.shift_right (index (vec_v p) 0) 64ul)))
+    (shift_right_i s (to_u64 (index (vec_v p) 0)))
   );
   reveal_vec_v_1 p;
   reveal_vec_v_1 (V.cast U128 1 (vec_shift_right (V.cast U64 2 p) s));
@@ -273,8 +351,8 @@ let lemma_vec128_shift_right_64 p s =
   let p0 = ((to_uint 128 a) % pow2 64) / pow2 (v s) in
   let p1 = (((to_uint 128 a) / pow2 64) % pow2 64) / pow2 (v s) in
   let t = T.add
-          (T.shift_left (to_u128 (shift_right_i s (to_u64 (T.shift_right #U128 #SEC p 64ul)))) 64ul)
-          (to_u128 (shift_right_i s (to_u64 #U128 #SEC p))) in
+          (to_u128 (shift_right_i s (to_u64 #U128 #SEC p)))
+          (T.shift_left (to_u128 (shift_right_i s (to_u64 (T.shift_right #U128 #SEC p 64ul)))) 64ul) in
   assert (t == V.cast U128 1 (vec_shift_right (V.cast U64 2 p) s));
   reveal_vec_v_1 #U128 t;
   assert (of_vec128 t == of_uint 128 (p1 * pow2 64 + p0));
diff --git a/lib/Lib.IntVector.fst b/lib/Lib.IntVector.fst
index 989eba9b05..2f050d5a39 100644
--- a/lib/Lib.IntVector.fst
+++ b/lib/Lib.IntVector.fst
@@ -332,9 +332,6 @@ let vec_interleave_high_n_lemma_uint64_4_2 v1 v2 = admit()
 
 let vec_shift_right_uint128_small2 v1 s = admit()
 
-let vec_cast_uint128 v1 = admit()
-let vec_cast_2_uint64 v1 = admit()
-
 let vec_permute2 #t v i1 i2 =
   match t with
   | U64 -> vec128_shuffle64 v i1 i2
@@ -453,3 +450,5 @@ let vec_store_be #t #w b v =
   | U32,8 -> vec256_store32_be b v
   | U64,4 -> vec256_store64_be b v
   | U128,2 -> admit() //vec256_store_be b v
+
+let cast_lemma #t #w t' w' v = admit()
diff --git a/lib/Lib.IntVector.fsti b/lib/Lib.IntVector.fsti
index 37bf61130c..b7813f15f4 100644
--- a/lib/Lib.IntVector.fsti
+++ b/lib/Lib.IntVector.fsti
@@ -16,7 +16,6 @@ inline_for_extraction
 val vec_t: t:v_inttype -> w:width -> Type0
 
 val reveal_vec_1: t:v_inttype -> Lemma
-  (requires t <> U128)
   (ensures vec_t t 1 == sec_int_t t)
 
 inline_for_extraction
@@ -43,7 +42,6 @@ val vecv_extensionality: #t:v_inttype -> #w:width -> f1:vec_t t w -> f2:vec_t t
   (ensures f1 == f2)
 
 val reveal_vec_v_1: #t:v_inttype -> f:vec_t t 1 -> Lemma
-  (requires t <> U128)
   (ensures (
     reveal_vec_1 t;
     f == index (vec_v f) 0))
@@ -259,15 +257,6 @@ val vec_shift_right_uint128_small2: v1:vec_t U64 4 -> s:shiftval U128{uint_v s %
      (((vec_v v1).[2] >>. s) |. ((vec_v v1).[3] <<. (64ul -! s)))
       ((vec_v v1).[3] >>. s))
 
-val vec_cast_uint128: v1:vec_t U128 1 -> Lemma
-  (vec_v (cast U64 2 v1) == create2
-     (to_u64 (vec_v v1).[0])
-     (to_u64 ((vec_v v1).[0] >>. 64ul)))
-
-val vec_cast_2_uint64: v1:vec_t U64 2 -> Lemma
-  (vec_v (cast U128 1 v1) == create 1
-     (((to_u128 (vec_v v1).[1]) <<. 64ul) +! (to_u128 (vec_v v1).[0])))
-
 inline_for_extraction
 val vec_permute2: #t:v_inttype -> v1:vec_t t 2
   -> i1:vec_index 2 -> i2:vec_index 2 ->
@@ -501,3 +490,7 @@ val vec_store_be:
   Stack unit
     (requires fun h -> live h b)
     (ensures  fun h0 r h1 -> h1 == h0 /\ as_seq h1 b == vec_to_bytes_be v)
+
+val cast_lemma: #t:v_inttype -> #w:width -> t':v_inttype -> w':width{bits t * w == bits t' * w'} -> v:vec_t t w ->
+  Lemma (cast t' w' v == vec_from_bytes_be t' w' (vec_to_bytes_be v))
+  [SMTPat (cast t' w' v)]