diff --git a/lib/Haskell/Extra/Dec.agda b/lib/Haskell/Extra/Dec.agda
index f13186ca..bfe228e7 100644
--- a/lib/Haskell/Extra/Dec.agda
+++ b/lib/Haskell/Extra/Dec.agda
@@ -1,19 +1,13 @@
 module Haskell.Extra.Dec where
 
 open import Haskell.Prelude hiding (Reflects)
+open import Haskell.Extra.Refinement
 open import Agda.Primitive
 
 @0 Reflects : ∀ {ℓ} → Set ℓ → Bool → Set ℓ
 Reflects P True  = P
 Reflects P False = P → ⊥
 
-record ∃ {ℓ ℓ′} (@0 a : Set ℓ) (@0 P : a → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
-  constructor _⟨_⟩
-  field
-    value    : a
-    @0 proof : P value
-open ∃ public
-{-# COMPILE AGDA2HS ∃ unboxed #-}
 
 Dec : ∀ {ℓ} → @0 Set ℓ → Set ℓ
 Dec P = ∃ Bool (Reflects P)
diff --git a/lib/Haskell/Extra/Refinement.agda b/lib/Haskell/Extra/Refinement.agda
new file mode 100644
index 00000000..52ee3e0a
--- /dev/null
+++ b/lib/Haskell/Extra/Refinement.agda
@@ -0,0 +1,15 @@
+module Haskell.Extra.Refinement where
+
+open import Haskell.Prelude
+open import Agda.Primitive
+
+private variable
+  ℓ ℓ′ : Level
+
+record ∃ (@0 a : Set ℓ) (@0 P : a → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
+  constructor _⟨_⟩
+  field
+    value    : a
+    @0 proof : P value
+open ∃ public
+{-# COMPILE AGDA2HS ∃ unboxed #-}