diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst
index 576cf0f58..85486df77 100644
--- a/lib/pulse/lib/Pulse.Lib.Slice.fst
+++ b/lib/pulse/lib/Pulse.Lib.Slice.fst
@@ -67,8 +67,8 @@ fn pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t)
 let is_from_array a s =
   AP.is_from_array s.elt (SZ.v s.len) a
 
-fn from_array (#t: Type) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
-  (alen: SZ.t { SZ.v alen == A.length a })
+fn from_array (#t: Type) (a: array t) (#p: perm) (alen: SZ.t)
+    (#v: Ghost.erased (Seq.seq t) { SZ.v alen == A.length a })
   requires A.pts_to a #p v
   returns s: (slice t)
   ensures 
diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti
index f219301e7..b7fc4794b 100644
--- a/lib/pulse/lib/Pulse.Lib.Slice.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti
@@ -36,7 +36,7 @@ val pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) : stt_ghost un
 
 val is_from_array (#t: Type) (a: array t) (s: slice t) : slprop
 
-val from_array (#t: Type) (a: array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (alen: SZ.t { SZ.v alen == A.length a }) : stt (slice t)
+val from_array (#t: Type) (a: array t) (#p: perm) (alen: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v alen == A.length a }) : stt (slice t)
     (A.pts_to a #p v)
     (fun s -> pts_to s #p v ** is_from_array a s)