diff --git a/proof-libs/fstar/core/Core.Array.fsti b/proof-libs/fstar/core/Core.Array.fsti
index e02274be0..b2b2f3e97 100644
--- a/proof-libs/fstar/core/Core.Array.fsti
+++ b/proof-libs/fstar/core/Core.Array.fsti
@@ -8,6 +8,6 @@ let impl_23__map #a n #b (arr: t_Array a n) (f: a -> b): t_Array b n
 
 let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 
-val from_fn #a len (f: usize -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
+val from_fn #a len (f: (x:usize{x <. len}) -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
     
 
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
index 2521af35f..d9d6b115c 100644
--- a/proof-libs/fstar/core/Core.Num.fsti
+++ b/proof-libs/fstar/core/Core.Num.fsti
@@ -2,6 +2,8 @@ module Core.Num
 open Rust_primitives
 
 let impl_u16__MAX: u16 = mk_u16 (maxint u16_inttype)
+let impl_i32__MAX: i32 = mk_i32 (maxint i32_inttype)
+let impl_i32__MIN: i32 = mk_i32 (minint i32_inttype)
 
 let impl_u8__wrapping_add: u8 -> u8 -> u8 = add_mod
 let impl_u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod