diff --git a/newt/Prelude.newt b/newt/Prelude.newt
index fe86a2d..ada883f 100644
--- a/newt/Prelude.newt
+++ b/newt/Prelude.newt
@@ -126,6 +126,17 @@ cong f Refl = Refl
 sym : ∀ A. {0 a b : A} → a ≡ b → b ≡ a
 sym Refl = Refl
 
+data Void : U where
+
+¬ : U → U
+¬ x = x → Void
+
+data Dec : U → U where
+  Yes : ∀ prop. (prf : prop) → Dec prop
+  No : ∀ prop. (contra : ¬ prop) → Dec prop
+
+class DecEq t where
+  decEq : (x₁ : t) → (x₂ : t) → Dec (x₁ ≡ x₂)
 
 
 -- Functor
diff --git a/tests/Neighbors.newt b/tests/Neighbors.newt
index 8c6d2fa..d337ece 100644
--- a/tests/Neighbors.newt
+++ b/tests/Neighbors.newt
@@ -4,8 +4,6 @@ module Neighbors
 -- Prf ?
 import Prelude
 
-data Void : U where
-
 data Prf : U → U where
   Pf : ∀ a. {{_ : a}} → Prf a
 
diff --git a/tests/RunLength.newt b/tests/RunLength.newt
index dd89740..0856fcd 100644
--- a/tests/RunLength.newt
+++ b/tests/RunLength.newt
@@ -6,22 +6,6 @@ module RunLength
 
 import Prelude
 
--- TODO this belongs in a library
-
-data Void : U where
-
-Not : U → U
-Not x = x → Void
-
-data Dec : U → U where
-  Yes : ∀ prop. (prf : prop) → Dec prop
-  No : ∀ prop. (contra : Not prop) → Dec prop
-
-class DecEq t where
-  decEq : (x₁ : t) → (x₂ : t) → Dec (x₁ ≡ x₂)
-
--- end lib
-
 rep : ∀ a. Nat → a → List a
 rep Z x = Nil
 rep (S k) x = x :: rep k x