diff --git a/nbe.rkt b/nbe.rkt
index 2c309dd..62bfb4c 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -168,4 +168,4 @@
 (define (β-eq? a b)
   (equal? (normalize a) (normalize b)))
 
-(provide reify interp normalize β-eq? Term D V βη-eq?)
+(provide reify interp normalize β-eq? Term D D-ne V βη-eq? ext subst1 subst idsub-tm)
diff --git a/type-checker.rkt b/type-checker.rkt
new file mode 100644
index 0000000..0ad77af
--- /dev/null
+++ b/type-checker.rkt
@@ -0,0 +1,2 @@
+#lang typed/racket
+(require "nbe.rkt")