diff --git a/numidr.ipkg b/numidr.ipkg
index 02c5245..f1a722a 100644
--- a/numidr.ipkg
+++ b/numidr.ipkg
@@ -10,8 +10,7 @@ langversion >= 0.6.0
 sourcedir = "src"
 readme = "README.md"
 
-modules = Data.NP,
-          Data.Permutation,
+modules = Data.Permutation,
           Data.NumIdr,
           Data.NumIdr.PrimArray,
           Data.NumIdr.PrimArray.Bytes,
diff --git a/sirdi.json b/sirdi.json
index 815929b..b65971f 100644
--- a/sirdi.json
+++ b/sirdi.json
@@ -4,7 +4,6 @@
     "version": "1.0.0",
     "deps": [],
     "modules": [
-      "Data.NP",
       "Data.Permutation",
       "Data.NumIdr",
       "Data.NumIdr.Array",
diff --git a/src/Data/NP.idr b/src/Data/NP.idr
deleted file mode 100644
index 6ee76e4..0000000
--- a/src/Data/NP.idr
+++ /dev/null
@@ -1,43 +0,0 @@
-module Data.NP
-
-import Data.Vect
-
-%default total
-
-
-||| A type constructor for heterogenous lists.
-public export
-data NP : (f : k -> Type) -> (ts : Vect n k) -> Type where
-  Nil  : NP {k} f []
-  (::) : f t -> NP {k} f ts -> NP {k} f (t :: ts)
-
-
-public export
-(all : NP (Eq . f) ts) => Eq (NP f ts) where
-  (==) {all=[]} [] [] = True
-  (==) {all=_::_} (x :: xs) (y :: ys) = (x == y) && (xs == ys)
-
-public export
-(all : NP (Show . f) ts) => Show (NP f ts) where
-  show xs = "[" ++ elems xs ++ "]"
-    where
-      elems : {0 f,ts : _} -> (all : NP (Show . f) ts) => NP f ts -> String
-      elems {all=[]} [] = ""
-      elems {all=[_]} [x] = show x
-      elems {all=_::_} (x :: xs) = show x ++ ", " ++ elems xs
-
--- use this when idris can't figure out the constraint above
-public export
-eqNP : forall f. (forall t. Eq (f t)) => (x, y : NP f ts) -> Bool
-eqNP [] [] = True
-eqNP (x :: xs) (y :: ys) = x == y && eqNP xs ys
-
-
-public export
-head : NP f (t :: ts) -> f t
-head (x :: _) = x
-
-public export
-index : (i : Fin n) -> NP {n} f ts -> f (index i ts)
-index FZ (x :: xs) = x
-index (FS i) (x :: xs) = index i xs
diff --git a/src/Data/NumIdr.idr b/src/Data/NumIdr.idr
index 2c5bc5f..9634f05 100644
--- a/src/Data/NumIdr.idr
+++ b/src/Data/NumIdr.idr
@@ -1,6 +1,5 @@
 module Data.NumIdr
 
-import public Data.NP
 import public Data.Permutation
 
 import public Data.NumIdr.Interfaces
diff --git a/src/Data/NumIdr/Array.idr b/src/Data/NumIdr/Array.idr
index 9efe967..12d6a1d 100644
--- a/src/Data/NumIdr/Array.idr
+++ b/src/Data/NumIdr/Array.idr
@@ -1,6 +1,5 @@
 module Data.NumIdr.Array
 
-import public Data.NP
 import public Data.NumIdr.Array.Array
 import public Data.NumIdr.Array.Coords
 import public Data.NumIdr.Array.Rep
diff --git a/src/Data/NumIdr/Array/Array.idr b/src/Data/NumIdr/Array/Array.idr
index e9ec0d9..fb33630 100644
--- a/src/Data/NumIdr/Array/Array.idr
+++ b/src/Data/NumIdr/Array/Array.idr
@@ -3,7 +3,6 @@ module Data.NumIdr.Array.Array
 import Data.List
 import Data.Vect
 import Data.Zippable
-import Data.NP
 import Data.Permutation
 import Data.NumIdr.Interfaces
 import Data.NumIdr.PrimArray
@@ -411,7 +410,7 @@ resize s' def arr = fromFunction {rep=getRep arr} @{getRepC arr} s' (fromMaybe d
 export
 -- HACK: Come up with a solution that doesn't use `believe_me` or trip over some
 -- weird bug in the type-checker
-resizeLTE : (s' : Vect rk Nat) -> (0 ok : NP Prelude.id (zipWith LTE s' s)) =>
+resizeLTE : (s' : Vect rk Nat) -> (0 ok : All Prelude.id (zipWith LTE s' s)) =>
             Array {rk} s a -> Array s' a
 resizeLTE s' arr = resize s' (believe_me ()) arr
 
diff --git a/src/Data/NumIdr/Array/Coords.idr b/src/Data/NumIdr/Array/Coords.idr
index 03b021e..669471a 100644
--- a/src/Data/NumIdr/Array/Coords.idr
+++ b/src/Data/NumIdr/Array/Coords.idr
@@ -4,7 +4,8 @@ import Data.Either
 import Data.List
 import Data.List1
 import Data.Vect
-import Data.NP
+
+import public Data.Vect.Quantifiers
 
 %default total
 
@@ -35,7 +36,16 @@ rangeLenZ x = rangeLen 0 x `trans` minusZeroRight x
 ||| values of `Fin dim`, where `dim` is the dimension of each axis.
 public export
 Coords : (s : Vect rk Nat) -> Type
-Coords = NP Fin
+Coords = All Fin
+
+
+-- Occasionally necessary for reasons of Idris not being great at
+-- resolving interface constraints
+public export
+[eqCoords] Eq (Coords s) where
+  [] == [] = True
+  (x :: xs) == (y :: ys) = x == y && xs == ys
+
 
 ||| Forget the shape of the array by converting each index to type `Nat`.
 export
@@ -63,7 +73,7 @@ namespace Strict
 
   public export
   CoordsRange : (s : Vect rk Nat) -> Type
-  CoordsRange = NP CRange
+  CoordsRange = All CRange
 
 
 namespace NB
diff --git a/src/Data/NumIdr/PrimArray.idr b/src/Data/NumIdr/PrimArray.idr
index 3fe2480..4ce2eb7 100644
--- a/src/Data/NumIdr/PrimArray.idr
+++ b/src/Data/NumIdr/PrimArray.idr
@@ -3,7 +3,6 @@ module Data.NumIdr.PrimArray
 import Data.Buffer
 import Data.Vect
 import Data.Fin
-import Data.NP
 import Data.NumIdr.Array.Rep
 import Data.NumIdr.Array.Coords
 import public Data.NumIdr.PrimArray.Bytes
@@ -98,7 +97,7 @@ indexUpdate {rep = Linked} is f arr = update is f arr
 indexUpdate {rep = Delayed} is f arr =
   \is' =>
     let x = arr is'
-    in if eqNP is is' then f x else x
+    in if (==) @{eqCoords} is is' then f x else x
 
 export
 indexRange : {rep,s : _} -> RepConstraint rep a => (rs : CoordsRange s) -> PrimArray rep s a
diff --git a/src/Data/NumIdr/PrimArray/Delayed.idr b/src/Data/NumIdr/PrimArray/Delayed.idr
index 96030e8..e90ae86 100644
--- a/src/Data/NumIdr/PrimArray/Delayed.idr
+++ b/src/Data/NumIdr/PrimArray/Delayed.idr
@@ -2,7 +2,6 @@ module Data.NumIdr.PrimArray.Delayed
 
 import Data.List
 import Data.Vect
-import Data.NP
 import Data.NumIdr.Array.Rep
 import Data.NumIdr.Array.Coords
 
diff --git a/src/Data/NumIdr/PrimArray/Linked.idr b/src/Data/NumIdr/PrimArray/Linked.idr
index 2e9817e..1fbce1b 100644
--- a/src/Data/NumIdr/PrimArray/Linked.idr
+++ b/src/Data/NumIdr/PrimArray/Linked.idr
@@ -2,7 +2,6 @@ module Data.NumIdr.PrimArray.Linked
 
 import Data.Vect
 import Data.DPair
-import Data.NP
 import Data.NumIdr.Array.Rep
 import Data.NumIdr.Array.Coords