diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fst b/lib/pulse/lib/Pulse.Lib.Array.Core.fst
index df1e229d0..38795b7cb 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.Core.fst
+++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fst
@@ -379,20 +379,29 @@ ghost fn pcm_gather u#a (#t: Type u#a) #l
 }
 
 ghost
-fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
-  requires pts_to_mask arr #p s mask
-  ensures pts_to_mask arr #(p /. 2.0R) s mask
-  ensures pts_to_mask arr #(p /. 2.0R) s mask
+fn mask_share_gen u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p (p1: perm) (p2: perm) #mask
+  requires pts_to_mask arr #p s mask ** pure ((p <: real) == p1 +. p2)
+  ensures pts_to_mask arr #p1 s mask
+  ensures pts_to_mask arr #p2 s mask
 {
   loc_get ();
   pts_to_mask_props arr;
   pcm_share
     arr p s mask
-    arr (p /. 2.0R) s mask
-    arr (p /. 2.0R) s mask;
+    arr p1 s mask
+    arr p2 s mask;
   drop_ (loc _);
 }
 
+ghost
+fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
+  requires pts_to_mask arr #p s mask
+  ensures pts_to_mask arr #(p /. 2.0R) s mask
+  ensures pts_to_mask arr #(p /. 2.0R) s mask
+{
+  mask_share_gen arr #s #p (p /. 2.0R) (p /. 2.0R) #mask
+}
+
 [@@allow_ambiguous]
 ghost fn mask_gather u#a (#t: Type u#a) (arr: array t) #p1 #p2 #s1 #s2 #mask1 #mask2
   requires pts_to_mask arr #p1 s1 mask1
diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fsti b/lib/pulse/lib/Pulse.Lib.Array.Core.fsti
index e67c7c735..29b2846cd 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.Core.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fsti
@@ -124,6 +124,12 @@ fn mask_free u#a (#elt: Type u#a) (a: array elt) (#s: Ghost.erased (Seq.seq elt)
   requires pure (forall i. mask i)
   requires pure (is_full_array a)
 
+ghost
+fn mask_share_gen u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p (p1: perm) (p2: perm) #mask
+  requires pts_to_mask arr #p s mask ** pure ((p <: real) == p1 +. p2)
+  ensures pts_to_mask arr #p1 s mask
+  ensures pts_to_mask arr #p2 s mask
+
 ghost
 fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
   requires pts_to_mask arr #p s mask
diff --git a/lib/pulse/lib/Pulse.Lib.Array.fst b/lib/pulse/lib/Pulse.Lib.Array.fst
index 8015d24d5..23502ca65 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.fst
+++ b/lib/pulse/lib/Pulse.Lib.Array.fst
@@ -53,7 +53,7 @@ fn compare (#t:eqtype) (l:US.t) (a1 a2:larray t (US.v l)) (#p1 #p2:perm)
   (!i = l)
 }
 
-fn memcpy_l (#t:eqtype) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
+fn memcpy_l (#t:Type0) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
            (#p:perm) (#src0 #dst0:Ghost.erased (Seq.seq t))
   requires pts_to src #p src0 **
            pts_to dst dst0
@@ -89,7 +89,7 @@ fn memcpy_l (#t:eqtype) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
 
 
 fn memcpy
-  (#t:eqtype)
+  (#t:Type0)
   (l:SZ.t)
   (src dst:larray t (SZ.v l))
   (#p:perm)
diff --git a/lib/pulse/lib/Pulse.Lib.Array.fsti b/lib/pulse/lib/Pulse.Lib.Array.fsti
index 12a978894..ee051d0d1 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Array.fsti
@@ -41,7 +41,7 @@ fn compare
      pure (res <==> Seq.equal s1 s2)
 
 fn memcpy_l
-        (#t:eqtype)
+        (#t:Type0)
         (l:SZ.t)
         (src dst:(a:array t { SZ.v l <= length a }))
         (#p:perm)
@@ -54,7 +54,7 @@ fn memcpy_l
                                    (Seq.slice dst0 (SZ.v l) (length dst)))
 
 fn memcpy
-        (#t:eqtype)
+        (#t:Type0)
         (l:SZ.t)
         (src dst:larray t (SZ.v l))
         (#p:perm)