diff --git a/sledge/lib/import/IArray.ml b/sledge/lib/import/IArray.ml
deleted file mode 100644
index 9097a4977..000000000
--- a/sledge/lib/import/IArray.ml
+++ /dev/null
@@ -1,125 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-(** IArray - Immutable view of an array *)
-
-open Import0
-
-(** = 'a array but covariant since imperative operations hidden *)
-type +'a t
-
-let v (a : 'a array) : 'a t = Obj.magic a
-let a (v : 'a t) : 'a array = Obj.magic v
-let _vl (al : 'a array list) : 'a t list = Obj.magic al
-let al (vl : 'a t list) : 'a array list = Obj.magic vl
-let compare cmp x y = Array.compare cmp (a x) (a y)
-let equal cmp x y = Array.equal cmp (a x) (a y)
-let hash_fold_t f s x = Hash.Builtin.hash_fold_array_frozen f s (a x)
-let t_of_sexp a_of_sexp s = v (Array.t_of_sexp a_of_sexp s)
-let sexp_of_t sexp_of_a x = Array.sexp_of_t sexp_of_a (a x)
-
-module Import = struct
-  type +'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
-end
-
-let to_list x = Array.to_list (a x)
-let to_array = a
-let pp sep pp_elt fs v = List.pp sep pp_elt fs (to_list v)
-let concat_map x ~f = v (Array.concat_map (a x) ~f:(fun y -> a (f y)))
-
-let combine_adjacent ~f xs_v =
-  let xs = a xs_v in
-  let n = Array.length xs - 1 in
-  let rec combine_adjacent_ j i xs =
-    if i < n then (
-      match f xs.(i - j) xs.(i + 1) with
-      | None ->
-          if j != 0 then xs.(i + 1 - j) <- xs.(i + 1) ;
-          combine_adjacent_ j (i + 1) xs
-      | Some x ->
-          let xs = if j = 0 then Array.copy xs else xs in
-          xs.(i - j) <- x ;
-          combine_adjacent_ (j + 1) (i + 1) xs )
-    else if j = 0 then xs
-    else Array.sub xs ~pos:0 ~len:(n + 1 - j)
-  in
-  v (combine_adjacent_ 0 0 xs)
-
-let create ~len x = v (Array.create ~len x)
-let empty = v [||]
-
-let contains_dup ~compare xs =
-  Option.is_some
-    (Array.find_consecutive_duplicate
-       ~equal:(fun x y -> compare x y = 0)
-       (Array.sorted_copy ~compare (a xs)))
-
-let find x ~f = Array.find (a x) ~f
-let find_exn x ~f = Array.find_exn (a x) ~f
-let find_map x ~f = Array.find_map (a x) ~f
-let fold x ~init ~f = Array.fold (a x) ~init ~f
-let fold_right x ~f ~init = Array.fold_right (a x) ~f ~init
-let fold_result x ~init ~f = Array.fold_result (a x) ~init ~f
-let fold_until x ~init ~f ~finish = Array.fold_until (a x) ~init ~f ~finish
-let fold2_exn x y ~init ~f = Array.fold2_exn (a x) (a y) ~init ~f
-let exists x ~f = Array.exists (a x) ~f
-let for_all x ~f = Array.for_all (a x) ~f
-let for_all2_exn x y ~f = Array.for_all2_exn (a x) (a y) ~f
-let filteri x ~f = v (Array.filteri (a x) ~f)
-
-external get : 'a t -> int -> 'a = "%array_safe_get"
-
-let last x = Array.last (a x)
-let init n ~f = v (Array.init n ~f)
-let is_empty x = Array.is_empty (a x)
-let iter x ~f = Array.iter (a x) ~f
-let rev_iter x ~f = Array.fold_right (a x) ~init:() ~f:(fun e () -> f e)
-let iter2_exn x y ~f = Array.iter2_exn (a x) (a y) ~f
-let iteri x ~f = Array.iteri (a x) ~f
-let length x = Array.length (a x)
-let map x ~f = v (Array.map (a x) ~f)
-
-let map_preserving_phys_equal xs ~f =
-  let change = ref false in
-  let xs' =
-    map xs ~f:(fun x ->
-        let x' = f x in
-        if not (x' == x) then change := true ;
-        x' )
-  in
-  if !change then xs' else xs
-
-let mapi x ~f = v (Array.mapi (a x) ~f)
-let map2_exn x y ~f = v (Array.map2_exn (a x) (a y) ~f)
-let map_inplace x ~f = Array.map_inplace (a x) ~f
-
-let fold_map x ~init ~f =
-  let s, x = Array.fold_map (a x) ~init ~f in
-  (s, v x)
-
-let fold_map_until xs ~init ~f ~finish =
-  with_return (fun {return} ->
-      finish
-        (fold_map xs ~init ~f:(fun s x ->
-             match (f s x : _ Continue_or_stop.t) with
-             | Continue x -> x
-             | Stop x -> return x )) )
-
-let concat xs = v (Array.concat (al xs))
-let copy x = v (Array.copy (a x))
-let sub ~pos ~len x = v (Array.sub ~pos ~len (a x))
-let subo ?pos ?len x = v (Array.subo ?pos ?len (a x))
-let of_ x = v [|x|]
-let of_array = v
-let of_list x = v (Array.of_list x)
-let of_list_rev x = v (Array.of_list_rev x)
-let of_option x = v (Option.to_array x)
-let reduce_exn x ~f = Array.reduce_exn (a x) ~f
-
-let unzip x =
-  let y, z = Array.unzip (a x) in
-  (v y, v z)
diff --git a/sledge/lib/import/IArray.mli b/sledge/lib/import/IArray.mli
deleted file mode 100644
index 7b9782c31..000000000
--- a/sledge/lib/import/IArray.mli
+++ /dev/null
@@ -1,198 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-(** IArray - Immutable view of an array
-
-    Note that vectors and arrays can be interconverted without copying. So
-    IArray is not a safe immutable data structure, it only attempts to make
-    it inconvenient to mutate. *)
-
-open Import0
-
-type +'a t [@@deriving compare, equal, hash, sexp]
-
-module Import : sig
-  type +'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
-end
-
-val pp : (unit, unit) fmt -> 'a pp -> 'a t pp
-
-(* val binary_search :
- *   ('a t, 'a, 'key) Base__Binary_searchable_intf.binary_search *)
-
-(* val binary_search_segmented :
- *   ('a t, 'a) Base__Binary_searchable_intf.binary_search_segmented *)
-
-(* val mem : 'a t -> 'a -> equal:('a -> 'a -> bool) -> bool *)
-
-val length : 'a t -> int
-val is_empty : 'a t -> bool
-val iter : 'a t -> f:('a -> unit) -> unit
-val rev_iter : 'a t -> f:('a -> unit) -> unit
-val fold : 'a t -> init:'accum -> f:('accum -> 'a -> 'accum) -> 'accum
-
-val fold_result :
-     'a t
-  -> init:'accum
-  -> f:('accum -> 'a -> ('accum, 'e) Result.t)
-  -> ('accum, 'e) Result.t
-
-val fold_until :
-     'a t
-  -> init:'accum
-  -> f:('accum -> 'a -> ('accum, 'final) Continue_or_stop.t)
-  -> finish:('accum -> 'final)
-  -> 'final
-
-val exists : 'a t -> f:('a -> bool) -> bool
-val for_all : 'a t -> f:('a -> bool) -> bool
-
-(* val count : 'a t -> f:('a -> bool) -> int *)
-
-(* val sum :
- *      (module Commutative_group.S with type t = 'sum)
- *   -> 'a t
- *   -> f:('a -> 'sum)
- *   -> 'sum *)
-
-val find : 'a t -> f:('a -> bool) -> 'a option
-val find_map : 'a t -> f:('a -> 'b option) -> 'b option
-val to_list : 'a t -> 'a list
-
-val to_array : 'a t -> 'a array
-(** [to_array v] is an array that shares its representation with vector [v],
-    therefore mutating [to_array v] changes [v] (as well as all the shallow
-    copies of [v] that are likely to exist). The intended use for [to_array]
-    is e.g. to pattern match on a vector, or to interface with some existing
-    array code that is known to not mutate its arguments. *)
-
-(* val min_elt : 'a t -> compare:('a -> 'a -> int) -> 'a option *)
-(* val max_elt : 'a t -> compare:('a -> 'a -> int) -> 'a option *)
-(* val invariant : 'a Base__Invariant_intf.inv -> 'a t
-   Base__Invariant_intf.inv *)
-(* val max_length : int *)
-
-external get : 'a t -> int -> 'a = "%array_safe_get"
-
-(* external unsafe_get : 'a t -> int -> 'a = "%array_unsafe_get" *)
-
-val create : len:int -> 'a -> 'a t
-val init : int -> f:(int -> 'a) -> 'a t
-
-(* val make_matrix : dimx:int -> dimy:int -> 'a -> 'a t t *)
-(* val append : 'a t -> 'a t -> 'a t *)
-
-val concat : 'a t list -> 'a t
-val copy : 'a t -> 'a t
-val sub : pos:int -> len:int -> 'a t -> 'a t
-val subo : ?pos:int -> ?len:int -> 'a t -> 'a t
-val of_ : 'a -> 'a t
-
-val of_array : 'a array -> 'a t
-(** [of_array a] is a vector that shares its representation with array [a],
-    therefore mutating [a] changes [of_array a]. The intended use for
-    [of_array] is for converting an array to a vector when the array will
-    not be used after conversion, or with care for multi-step initialization
-    of a vector. *)
-
-val of_list : 'a list -> 'a t
-val of_option : 'a option -> 'a t
-val map : 'a t -> f:('a -> 'b) -> 'b t
-
-val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t
-(** Like map, but preserves [phys_equal] if [f] preserves [phys_equal] of
-    every element. *)
-
-(* val folding_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'c t *)
-(* val folding_mapi : 'a t -> init:'b -> f:(int -> 'b -> 'a -> 'b * 'c) ->
-   'c t *)
-
-val fold_map_until :
-     'a t
-  -> init:'accum
-  -> f:('accum -> 'a -> ('accum * 'b, 'final) Continue_or_stop.t)
-  -> finish:('accum * 'b t -> 'final)
-  -> 'final
-
-val fold_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'b * 'c t
-
-(* val fold_mapi :
- *   'a t -> init:'b -> f:(int -> 'b -> 'a -> 'b * 'c) -> 'b * 'c t *)
-
-val iteri : 'a t -> f:(int -> 'a -> unit) -> unit
-val mapi : 'a t -> f:(int -> 'a -> 'b) -> 'b t
-
-(* val foldi : 'a t -> init:'b -> f:(int -> 'b -> 'a -> 'b) -> 'b *)
-
-val fold_right : 'a t -> f:('a -> 'b -> 'b) -> init:'b -> 'b
-
-(* val is_sorted : 'a t -> compare:('a -> 'a -> int) -> bool *)
-(* val is_sorted_strictly : 'a t -> compare:('a -> 'a -> int) -> bool *)
-
-val concat_map : 'a t -> f:('a -> 'b t) -> 'b t
-
-(* val concat_mapi : 'a t -> f:(int -> 'a -> 'b t) -> 'b t *)
-
-val combine_adjacent : f:('a -> 'a -> 'a option) -> 'a t -> 'a t
-
-(* val partition_tf : 'a t -> f:('a -> bool) -> 'a t * 'a t *)
-(* val partitioni_tf : 'a t -> f:(int -> 'a -> bool) -> 'a t * 'a t *)
-(* val cartesian_product : 'a t -> 'b t -> ('a * 'b) t *)
-(* val transpose : 'a t t -> 'a t t option *)
-(* val transpose_exn : 'a t t -> 'a t t *)
-(* val filter_opt : 'a option t -> 'a t *)
-(* val filter_map : 'a t -> f:('a -> 'b option) -> 'b t *)
-(* val filter_mapi : 'a t -> f:(int -> 'a -> 'b option) -> 'b t *)
-(* val for_alli : 'a t -> f:(int -> 'a -> bool) -> bool *)
-(* val existsi : 'a t -> f:(int -> 'a -> bool) -> bool *)
-(* val counti : 'a t -> f:(int -> 'a -> bool) -> int *)
-
-val iter2_exn : 'a t -> 'b t -> f:('a -> 'b -> unit) -> unit
-val map2_exn : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t
-val fold2_exn : 'a t -> 'b t -> init:'c -> f:('c -> 'a -> 'b -> 'c) -> 'c
-val for_all2_exn : 'a t -> 'b t -> f:('a -> 'b -> bool) -> bool
-
-(* val exists2_exn : 'a t -> 'b t -> f:('a -> 'b -> bool) -> bool *)
-(* val filter : 'a t -> f:('a -> bool) -> 'a t *)
-val filteri : 'a t -> f:(int -> 'a -> bool) -> 'a t
-val of_list_rev : 'a list -> 'a t
-
-(* val of_list_map : 'a list -> f:('a -> 'b) -> 'b t *)
-(* val of_list_rev_map : 'a list -> f:('a -> 'b) -> 'b t *)
-
-val map_inplace : 'a t -> f:('a -> 'a) -> unit
-val find_exn : 'a t -> f:('a -> bool) -> 'a
-
-(* val find_map_exn : 'a t -> f:('a -> 'b option) -> 'b *)
-(* val findi : 'a t -> f:(int -> 'a -> bool) -> (int * 'a) option *)
-(* val findi_exn : 'a t -> f:(int -> 'a -> bool) -> int * 'a *)
-(* val find_mapi : 'a t -> f:(int -> 'a -> 'b option) -> 'b option *)
-(* val find_mapi_exn : 'a t -> f:(int -> 'a -> 'b option) -> 'b *)
-
-(* val find_consecutive_duplicate :
- *   'a t -> equal:('a -> 'a -> bool) -> ('a * 'a) option *)
-
-val contains_dup : compare:('a -> 'a -> int) -> 'a t -> bool
-
-(* val reduce : 'a t -> f:('a -> 'a -> 'a) -> 'a option *)
-val reduce_exn : 'a t -> f:('a -> 'a -> 'a) -> 'a
-
-(* val random_element :
- *   ?random_state:Base.Random.State.t -> 'a t -> 'a option *)
-
-(* val random_element_exn : ?random_state:Base.Random.State.t -> 'a t -> 'a *)
-(* val zip : 'a t -> 'b t -> ('a * 'b) t option *)
-(* val zip_exn : 'a t -> 'b t -> ('a * 'b) t *)
-
-val unzip : ('a * 'b) t -> 'a t * 'b t
-
-(* val sorted_copy : 'a t -> compare:('a -> 'a -> int) -> 'a t *)
-val last : 'a t -> 'a
-val empty : 'a t
-
-(* val to_sequence : 'a t -> 'a Sequence.t *)
-(* val to_sequence_mutable : 'a t -> 'a Sequence.t *)
diff --git a/sledge/lib/import/iArray.ml b/sledge/lib/import/iArray.ml
new file mode 100644
index 000000000..e37e906f8
--- /dev/null
+++ b/sledge/lib/import/iArray.ml
@@ -0,0 +1,80 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** IArray - Immutable view of an array *)
+
+open Import0
+
+include (
+  Array.Permissioned :
+    module type of Array.Permissioned
+      with type ('a, 'p) t := ('a, 'p) Array.Permissioned.t )
+
+type 'a t = ('a, immutable) Array.Permissioned.t
+
+let a2i (a : 'a array) : 'a t = Obj.magic a
+let i2a (a : 'a t) : 'a array = Obj.magic a
+let compare compare_elt = compare compare_elt compare_immutable
+
+let hash_fold_t hash_fold_elt s (a : _ t) =
+  Hash.Builtin.hash_fold_array_frozen hash_fold_elt s (i2a a)
+
+let t_of_sexp elt_of_sexp = t_of_sexp elt_of_sexp immutable_of_sexp
+let sexp_of_t sexp_of_elt = sexp_of_t sexp_of_elt sexp_of_immutable
+
+module Import = struct
+  type 'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
+end
+
+let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
+let empty = Obj.magic [||]
+let of_ x = create ~len:1 x
+let of_array = a2i
+
+let contains_dup ~compare xs =
+  let equal x y = compare x y = 0 in
+  Option.is_some
+    (find_consecutive_duplicate ~equal (sorted_copy ~compare xs))
+
+let fold_map xs ~init ~f =
+  Tuple2.map_snd ~f:a2i (Array.fold_map (i2a xs) ~init ~f)
+
+let fold_map_until xs ~init ~f ~finish =
+  with_return (fun {return} ->
+      finish
+        (fold_map xs ~init ~f:(fun s x ->
+             match (f s x : _ Continue_or_stop.t) with
+             | Continue x -> x
+             | Stop x -> return x )) )
+
+let map_preserving_phys_equal xs ~f =
+  let change = ref false in
+  let xs' =
+    map xs ~f:(fun x ->
+        let x' = f x in
+        if not (x' == x) then change := true ;
+        x' )
+  in
+  if !change then xs' else xs
+
+let combine_adjacent ~f xs =
+  let xs = i2a xs in
+  let n = Array.length xs - 1 in
+  let rec combine_adjacent_ j i xs =
+    if i < n then (
+      match f xs.(i - j) xs.(i + 1) with
+      | None ->
+          if j != 0 then xs.(i + 1 - j) <- xs.(i + 1) ;
+          combine_adjacent_ j (i + 1) xs
+      | Some x ->
+          let xs = if j = 0 then Array.copy xs else xs in
+          xs.(i - j) <- x ;
+          combine_adjacent_ (j + 1) (i + 1) xs )
+    else if j = 0 then xs
+    else Array.sub xs ~pos:0 ~len:(n + 1 - j)
+  in
+  a2i (combine_adjacent_ 0 0 xs)
diff --git a/sledge/lib/import/iArray.mli b/sledge/lib/import/iArray.mli
new file mode 100644
index 000000000..bf0863fb6
--- /dev/null
+++ b/sledge/lib/import/iArray.mli
@@ -0,0 +1,56 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** IArray - Immutable view of an array
+
+    Note that an iarray can be constructed from an array without copying,
+    and the client might keep other references to the backing array and use
+    them to later modify it. So IArray is not a safe immutable data
+    structure, it only attempts to make it inconvenient to unintentionally
+    mutate. *)
+
+open Import0
+
+include
+  module type of Array.Permissioned
+    with type ('a, 'p) t := ('a, 'p) Array.Permissioned.t
+
+type 'a t = ('a, immutable) Array.Permissioned.t
+[@@deriving compare, equal, hash, sexp]
+
+module Import : sig
+  type 'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
+end
+
+val pp : (unit, unit) fmt -> 'a pp -> 'a t pp
+val empty : 'a t
+val of_ : 'a -> 'a t
+
+val of_array : 'a array -> 'a t
+(** [of_array a] is an iarray that shares its representation with array [a],
+    therefore mutating [a] changes [of_array a]. The intended use for
+    [of_array] is for converting an array to an iarray when the array will
+    not be used after conversion, or with care for multi-step initialization
+    of an iarray. *)
+
+val contains_dup : compare:('a -> 'a -> int) -> 'a t -> bool
+
+val fold_map :
+  'a t -> init:'accum -> f:('accum -> 'a -> 'accum * 'b) -> 'accum * 'b t
+
+val fold_map_until :
+     'a t
+  -> init:'accum
+  -> f:('accum -> 'a -> ('accum * 'b, 'final) Continue_or_stop.t)
+  -> finish:('accum * 'b t -> 'final)
+  -> 'final
+
+val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t
+(** Like map, but preserves [phys_equal] if [f] preserves [phys_equal] of
+    every element. *)
+
+val combine_adjacent : f:('a -> 'a -> 'a option) -> 'a t -> 'a t
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index b2bca8fc5..77dd0a2c4 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -1084,11 +1084,11 @@ let map_rec_pre ~f e =
       | RecN (op, xs) -> (
         match List.Assoc.find ~equal:( == ) memo e with
         | None ->
-            let xs' = IArray.copy xs in
-            let e' = RecN (op, xs') in
+            let xs' = IArray.to_array xs in
+            let e' = RecN (op, IArray.of_array xs') in
             let memo = List.Assoc.add ~equal:( == ) memo e e' in
             let changed = ref false in
-            IArray.map_inplace xs' ~f:(fun x ->
+            Array.map_inplace xs' ~f:(fun x ->
                 let x' = map_rec_pre_f memo x in
                 if x' != x then changed := true ;
                 x' ) ;