diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
new file mode 100644
index 0000000..ba1e892
--- /dev/null
+++ b/src/Quox/Eval.idr
@@ -0,0 +1,30 @@
+module Quox.Eval
+
+-- todo list:
+-- - understand nbe and use it
+-- - take a proof of well-typedness as an argument
+
+import Quox.Syntax
+
+import Data.DPair
+
+%default total
+
+
+public export Exists2 : (ty1 -> ty2 -> Type) -> Type
+Exists2 t = Exists (\a => Exists (\b => t a b))
+
+public export SomeTerm : Type
+SomeTerm = Exists2 Term
+
+public export SomeElim : Type
+SomeElim = Exists2 Elim
+
+public export SomeDim : Type
+SomeDim = Exists Dim
+
+private some : {0 t : ty -> Type} -> t a -> Exists t
+some t = Evidence ? t
+
+private some2 : {0 t : ty1 -> ty2 -> Type} -> t a b -> Exists2 t
+some2 t = some $ some t