diff --git a/README.md b/README.md
index 859cb3c..6894098 100644
--- a/README.md
+++ b/README.md
@@ -15,20 +15,30 @@ cur (plural curs)
 Disclaimer
 ==========
 Cur is currently under active hackery and is not fit for use for any
-particular purpose. It is fraught with unreadable code, errors, and
-hacks that should never have been written by a reasonable human being.
+particular purpose. It is fraught with unreadable code, errors,
+performance bugs, and hacks that should never have been written by a
+reasonable human being.
 These may or may not be fixed shortly.
 
 Getting started
 ===============
 
+Easy mode:
 Install cur via `raco pkg install cur`.
 
+Advanced mode:
+Cur is actually distributed as several packages.
+`cur-lib` provides the implementation and all standard
+libraries.
+`cur-doc` provides the documentation.
+`cur-test` provides a test suite and examples.
+
+
 Try it out: open up DrRacket and put the following in the definition area:
 
 ```racket
 #lang cur
-(require 
+(require
  cur/stdlib/bool
  cur/stdlib/nat)
 
@@ -44,27 +54,20 @@ Try entering the following in the interaction area:
 
 See the docs: `raco docs cur`.
 
-Most of the standard library is currently undocumented, so just see the source.
-
 Going further
 =============
 
-Open up `examples/example.rkt` to see a tour of Cur's features.
-
-Open up `examples/stlc.rkt` to see an example of what advanced meta-programming can let you do.
-
-Open up `oll.rkt` to see the implementation of the meta-programs used to
-enable `examples/stlc.rkt`, including the parsers for BNF syntax and inference rule
-syntax, and Coq and LaTeX generators.
+Open up `cur-tests/cur/tests/stlc.rkt` to see an example of the
+simply-typed lambda-calculus modeled in Cur, with a parser and syntax
+extension to enable deeply embedding.
 
 Open up `examples/proofs-for-free.rkt` to see an implementation of the
 translation defined in [Proofs for Free](http://staff.city.ac.uk/~ross/papers/proofs.html) as a meta-program.
 
-Open up `stdlib/tactics` to see tactics, implemented entirely via
-meta-programming.
+Open up `cur-lib/cur/stdlib/tactics` to see one way to implement tactics in Cur.
 
-Open up anything in `stdlib/` to see some standard dependent-type
+Open up anything in `cur-lib/cur/stdlib/` to see some standard dependent-type
 formalisms.
 
-Open up `curnel/redex-core.rkt` to see the entire "trusted" (after a
-large test suite) core.
+Open up `cur-lib/cur/curnel/redex-core.rkt` to see the entire
+implementation of the core language, <600 lines of code.
diff --git a/scribblings/cur.scrbl b/cur-doc/cur/cur.scrbl
similarity index 91%
rename from scribblings/cur.scrbl
rename to cur-doc/cur/cur.scrbl
index f3fcc76..bd335ac 100644
--- a/scribblings/cur.scrbl
+++ b/cur-doc/cur/cur.scrbl
@@ -1,6 +1,6 @@
 #lang scribble/manual
 @(require
-   "defs.rkt"
+   "scribblings/defs.rkt"
    racket/function)
 
 @title[#:style '(toc)]{Cur}
@@ -42,7 +42,7 @@ Everything else in @racketmodname[cur] is provided by untrusted user-land code--
 
 @local-table-of-contents[]
 
-@include-section{curnel.scrbl}
-@include-section{reflection.scrbl}
-@include-section{stdlib.scrbl}
-@include-section{oll.scrbl}
+@include-section{scribblings/curnel.scrbl}
+@include-section{scribblings/reflection.scrbl}
+@include-section{scribblings/stdlib.scrbl}
+@include-section{scribblings/oll.scrbl}
diff --git a/cur-doc/cur/info.rkt b/cur-doc/cur/info.rkt
new file mode 100644
index 0000000..843460e
--- /dev/null
+++ b/cur-doc/cur/info.rkt
@@ -0,0 +1,2 @@
+#lang info
+(define scribblings '(("cur.scrbl" (multi-page))))
diff --git a/scribblings/curnel.scrbl b/cur-doc/cur/scribblings/curnel.scrbl
similarity index 100%
rename from scribblings/curnel.scrbl
rename to cur-doc/cur/scribblings/curnel.scrbl
diff --git a/scribblings/defs.rkt b/cur-doc/cur/scribblings/defs.rkt
similarity index 100%
rename from scribblings/defs.rkt
rename to cur-doc/cur/scribblings/defs.rkt
diff --git a/scribblings/oll.scrbl b/cur-doc/cur/scribblings/oll.scrbl
similarity index 100%
rename from scribblings/oll.scrbl
rename to cur-doc/cur/scribblings/oll.scrbl
diff --git a/scribblings/reflection.scrbl b/cur-doc/cur/scribblings/reflection.scrbl
similarity index 100%
rename from scribblings/reflection.scrbl
rename to cur-doc/cur/scribblings/reflection.scrbl
diff --git a/scribblings/stdlib.scrbl b/cur-doc/cur/scribblings/stdlib.scrbl
similarity index 100%
rename from scribblings/stdlib.scrbl
rename to cur-doc/cur/scribblings/stdlib.scrbl
diff --git a/scribblings/stdlib/bool.scrbl b/cur-doc/cur/scribblings/stdlib/bool.scrbl
similarity index 100%
rename from scribblings/stdlib/bool.scrbl
rename to cur-doc/cur/scribblings/stdlib/bool.scrbl
diff --git a/scribblings/stdlib/maybe.scrbl b/cur-doc/cur/scribblings/stdlib/maybe.scrbl
similarity index 100%
rename from scribblings/stdlib/maybe.scrbl
rename to cur-doc/cur/scribblings/stdlib/maybe.scrbl
diff --git a/scribblings/stdlib/nat.scrbl b/cur-doc/cur/scribblings/stdlib/nat.scrbl
similarity index 100%
rename from scribblings/stdlib/nat.scrbl
rename to cur-doc/cur/scribblings/stdlib/nat.scrbl
diff --git a/scribblings/stdlib/sugar.scrbl b/cur-doc/cur/scribblings/stdlib/sugar.scrbl
similarity index 100%
rename from scribblings/stdlib/sugar.scrbl
rename to cur-doc/cur/scribblings/stdlib/sugar.scrbl
diff --git a/scribblings/stdlib/tactics.scrbl b/cur-doc/cur/scribblings/stdlib/tactics.scrbl
similarity index 100%
rename from scribblings/stdlib/tactics.scrbl
rename to cur-doc/cur/scribblings/stdlib/tactics.scrbl
diff --git a/scribblings/stdlib/typeclass.scrbl b/cur-doc/cur/scribblings/stdlib/typeclass.scrbl
similarity index 100%
rename from scribblings/stdlib/typeclass.scrbl
rename to cur-doc/cur/scribblings/stdlib/typeclass.scrbl
diff --git a/cur-doc/info.rkt b/cur-doc/info.rkt
new file mode 100644
index 0000000..0cf5446
--- /dev/null
+++ b/cur-doc/info.rkt
@@ -0,0 +1,6 @@
+#lang info
+(define collection 'multi)
+(define deps '("base" "racket-doc"))
+(define build-deps '("scribble-lib" ("cur-lib" #:version "0.2") "sandbox-lib"))
+(define pkg-desc "Documentation for \"cur\".")
+(define pkg-authors '(wilbowma))
diff --git a/cur.rkt b/cur-lib/cur/cur.rkt
similarity index 100%
rename from cur.rkt
rename to cur-lib/cur/cur.rkt
diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt
new file mode 100644
index 0000000..47352a3
--- /dev/null
+++ b/cur-lib/cur/curnel/redex-core.rkt
@@ -0,0 +1,590 @@
+#lang racket/base
+
+(require
+  racket/function
+  redex/reduction-semantics)
+
+(provide
+  (all-defined-out))
+
+(set-cache-size! 10000)
+
+#| References:
+ |  http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
+ |  https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf
+ |  http://www.emn.fr/z-info/ntabareau/papers/universe_polymorphism.pdf
+ |  http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf
+ |  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.74
+ |  http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf
+ |#
+
+#| ttL is the core language of Cur. Very similar to TT (Idirs core) and Luo's UTT. Surface
+ | langauge should provide short-hand, such as -> for non-dependent function types, and type
+ | inference.
+ |#
+(define-language ttL
+  (i j k  ::= natural)
+  (U ::= (Unv i))
+  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e) (elim D U))
+  ;; Δ (signature). (inductive-name : type ((constructor : type) ...))
+  ;; NB: Δ is a map from a name x to a pair of it's type and a map of constructor names to their types
+  (Δ   ::= ∅ (Δ (D : t ((c : t) ...))))
+  (D x c ::= variable-not-otherwise-mentioned)
+  #:binding-forms
+  (λ (x : t) e #:refers-to x)
+  (Π (x : t_0) t_1 #:refers-to x))
+
+(define x? (redex-match? ttL x))
+(define t? (redex-match? ttL t))
+(define e? (redex-match? ttL e))
+(define U? (redex-match? ttL U))
+(define Δ? (redex-match? ttL Δ))
+
+;;; ------------------------------------------------------------------------
+;;; Universe typing
+
+(define-judgment-form ttL
+  #:mode (unv-type I O)
+  #:contract (unv-type U U)
+
+  [(where i_1 ,(add1 (term i_0)))
+   -----------------
+   (unv-type (Unv i_0) (Unv i_1))])
+
+;; Universe predicativity rules. Impredicative in (Unv 0)
+(define-judgment-form ttL
+  #:mode (unv-pred I I O)
+  #:contract (unv-pred U U U)
+
+  [----------------
+   (unv-pred (Unv i) (Unv 0) (Unv 0))]
+
+  [(where i_3 ,(max (term i_1) (term i_2)))
+   ----------------
+   (unv-pred (Unv i_1) (Unv i_2) (Unv i_3))])
+
+(define-metafunction ttL
+  α-equivalent?  : t t -> #t or #f
+  [(α-equivalent? t_0 t_1)
+   ,(alpha-equivalent? ttL (term t_0) (term t_1))])
+
+;; Replace x by t_1 in t_0
+(define-metafunction ttL
+  subst : t x t -> t
+  [(subst t_0 x t_1)
+   (substitute t_0 x t_1)])
+
+(define-metafunction ttL
+  subst-all : t (x ...) (e ...) -> t
+  [(subst-all t () ()) t]
+  [(subst-all t (x_0 x ...) (e_0 e ...))
+   (subst-all (subst t x_0 e_0) (x ...) (e ...))])
+
+;;; ------------------------------------------------------------------------
+;;; Primitive Operations on signatures Δ (those operations that do not require contexts)
+
+;;; TODO: Might be worth maintaining the above bijection between Δ and maps for performance reasons
+
+;; TODO: This is doing too many things
+;; NB: Depends on clause order
+(define-metafunction ttL
+  Δ-ref-type : Δ x -> t or #f
+  [(Δ-ref-type ∅ x) #f]
+  [(Δ-ref-type (Δ (x : t any)) x) t]
+  [(Δ-ref-type (Δ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t]
+  [(Δ-ref-type (Δ (x_0 : t_0 any)) x) (Δ-ref-type Δ x)])
+
+(define-metafunction ttL
+  Δ-set : Δ x t ((x : t) ...) -> Δ
+  [(Δ-set Δ x t any) (Δ (x : t any))])
+
+(define-metafunction ttL
+  Δ-union : Δ Δ -> Δ
+  [(Δ-union Δ ∅) Δ]
+  [(Δ-union Δ_2 (Δ_1 (x : t any)))
+   ((Δ-union Δ_2 Δ_1) (x : t any))])
+
+;; Returns the inductively defined type that x constructs
+;; NB: Depends on clause order
+(define-metafunction ttL
+  Δ-key-by-constructor : Δ x -> x
+  [(Δ-key-by-constructor (Δ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c)
+   x]
+  [(Δ-key-by-constructor (Δ (x_1 : t_1 any)) x)
+   (Δ-key-by-constructor Δ x)])
+
+;; Returns the constructor map for the inductively defined type x_D in the signature Δ
+(define-metafunction ttL
+  Δ-ref-constructor-map : Δ x -> ((x : t) ...) or #f
+  ;; NB: Depends on clause order
+  [(Δ-ref-constructor-map ∅ x_D) #f]
+  [(Δ-ref-constructor-map (Δ (x_D : t_D any)) x_D)
+   any]
+  [(Δ-ref-constructor-map (Δ (x_1 : t_1 any)) x_D)
+   (Δ-ref-constructor-map Δ x_D)])
+
+;; TODO: Should not use Δ-ref-type
+(define-metafunction ttL
+  Δ-ref-constructor-type : Δ x x -> t
+  [(Δ-ref-constructor-type Δ x_D x_ci)
+   (Δ-ref-type Δ x_ci)])
+
+;; Get the list of constructors for the inducitvely defined type x_D
+;; NB: Depends on clause order
+(define-metafunction ttL
+  Δ-ref-constructors : Δ x -> (x ...) or #f
+  [(Δ-ref-constructors ∅ x_D) #f]
+  [(Δ-ref-constructors (Δ (x_D : t_D ((x : t) ...))) x_D)
+   (x ...)]
+  [(Δ-ref-constructors (Δ (x_1 : t_1 any)) x_D)
+   (Δ-ref-constructors Δ x_D)])
+
+;; NB: Depends on clause order
+(define-metafunction ttL
+  sequence-index-of : any (any ...) -> natural
+  [(sequence-index-of any_0 (any_0 any ...))
+   0]
+  [(sequence-index-of any_0 (any_1 any ...))
+   ,(add1 (term (sequence-index-of any_0 (any ...))))])
+
+;; Get the index of the constructor x_ci in the list of constructors for x_D
+(define-metafunction ttL
+  Δ-constructor-index : Δ x x -> natural
+  [(Δ-constructor-index Δ x_D x_ci)
+   (sequence-index-of x_ci (Δ-ref-constructors Δ x_D))])
+
+;;; ------------------------------------------------------------------------
+;;; Operations that involve contexts.
+
+(define-extended-language tt-ctxtL ttL
+  ;; Telescope.
+  ;; NB: There is a bijection between this an a vector of maps from x to t
+  (Ξ Φ ::= hole (Π (x : t) Ξ))
+  ;; Apply context
+  ;; NB: There is a bijection between this an a vector expressions
+  (Θ   ::= hole (Θ e)))
+
+(define Ξ? (redex-match? tt-ctxtL Ξ))
+(define Φ? (redex-match? tt-ctxtL Φ))
+(define Θ? (redex-match? tt-ctxtL Θ))
+
+;; TODO: Might be worth it to actually maintain the above bijections, for performance reasons.
+
+;; Return the parameters of x_D as a telescope Ξ
+;; TODO: Define generic traversals of Δ and Γ ?
+(define-metafunction tt-ctxtL
+  Δ-ref-parameter-Ξ : Δ x -> Ξ
+  [(Δ-ref-parameter-Ξ (Δ (x_D : (in-hole Ξ U) any)) x_D)
+   Ξ]
+  [(Δ-ref-parameter-Ξ (Δ (x_1 : t_1 any)) x_D)
+   (Δ-ref-parameter-Ξ Δ x_D)])
+
+;; Applies the term t to the telescope Ξ.
+;; TODO: Test
+#| TODO:
+ | This essentially eta-expands t at the type-level. Why is this necessary? Shouldn't it be true
+ | that (equivalent t (Ξ-apply Ξ t))?
+ | Maybe not. t is a lambda whose type is equivalent to (Ξ-apply Ξ t)? Yes.
+ |#
+(define-metafunction tt-ctxtL
+  Ξ-apply : Ξ t -> t
+  [(Ξ-apply hole t) t]
+  [(Ξ-apply (Π (x : t) Ξ) t_0) (Ξ-apply Ξ (t_0 x))])
+
+;; Compose multiple telescopes into a single telescope:
+(define-metafunction tt-ctxtL
+  Ξ-compose : Ξ Ξ ... -> Ξ
+  [(Ξ-compose Ξ) Ξ]
+  [(Ξ-compose Ξ_0 Ξ_1 Ξ_rest ...)
+   (Ξ-compose (in-hole Ξ_0 Ξ_1) Ξ_rest ...)])
+
+;; Compute the number of arguments in a Ξ
+(define-metafunction tt-ctxtL
+  Ξ-length : Ξ -> natural
+  [(Ξ-length hole) 0]
+  [(Ξ-length (Π (x : t) Ξ)) ,(add1 (term (Ξ-length Ξ)))])
+
+;; Compute the number of applications in a Θ
+(define-metafunction tt-ctxtL
+  Θ-length : Θ -> natural
+  [(Θ-length hole) 0]
+  [(Θ-length (Θ e)) ,(add1 (term (Θ-length Θ)))])
+
+;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole.
+(define-metafunction tt-ctxtL
+  Θ-ref : Θ natural -> e or #f
+  [(Θ-ref hole natural) #f]
+  [(Θ-ref (in-hole Θ (hole e)) 0) e]
+  [(Θ-ref (in-hole Θ (hole e)) natural) (Θ-ref Θ ,(sub1 (term natural)))])
+
+;;; ------------------------------------------------------------------------
+;;; Computing the types of eliminators
+
+;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-telescope : Δ x x -> Ξ
+  [(Δ-constructor-telescope Δ x_D x_ci)
+   Ξ
+   (where (in-hole Ξ (in-hole Θ x_D))
+     (Δ-ref-constructor-type Δ x_D x_ci))])
+
+;; Returns the parameter arguments as an apply context of the constructor x_ci of the inductively
+;; defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-parameters : Δ x x -> Θ
+  [(Δ-constructor-parameters Δ x_D x_ci)
+   Θ
+   (where (in-hole Ξ (in-hole Θ x_D))
+     (Δ-ref-constructor-type Δ x_D x_ci))])
+
+;; Inner loop for Δ-constructor-noninductive-telescope
+(define-metafunction tt-ctxtL
+  noninductive-loop : x Φ -> Φ
+  [(noninductive-loop x_D hole) hole]
+  [(noninductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
+   (noninductive-loop x_D Φ_1)]
+  [(noninductive-loop x_D (Π (x : t) Φ_1))
+   (Π (x : t) (noninductive-loop x_D Φ_1))])
+
+;; Returns the noninductive arguments to the constructor x_ci of the inductively defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-noninductive-telescope : Δ x x -> Ξ
+  [(Δ-constructor-noninductive-telescope Δ x_D x_ci)
+   (noninductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
+
+;; Inner loop for Δ-constructor-inductive-telescope
+;; NB: Depends on clause order
+(define-metafunction tt-ctxtL
+  inductive-loop : x Φ -> Φ
+  [(inductive-loop x_D hole) hole]
+  [(inductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
+   (Π (x : (in-hole Φ (in-hole Θ x_D))) (inductive-loop x_D Φ_1))]
+  [(inductive-loop x_D (Π (x : t) Φ_1))
+   (inductive-loop x_D Φ_1)])
+
+;; Returns the inductive arguments to the constructor x_ci of the inducitvely defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-inductive-telescope : Δ x x -> Ξ
+  [(Δ-constructor-inductive-telescope Δ x_D x_ci)
+   (inductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
+
+;; Returns the inductive hypotheses required for eliminating the inductively defined type x_D with
+;; motive t_P, where the telescope Φ are the inductive arguments to a constructor for x_D
+(define-metafunction tt-ctxtL
+  hypotheses-loop : x t Φ -> Φ
+  [(hypotheses-loop x_D t_P hole) hole]
+  [(hypotheses-loop x_D t_P (name any_0 (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1)))
+   ;; TODO: Instead of this nonsense, it might be simpler to pass in the type of t_P and use that
+   ;; as/to compute the type of the hypothesis.
+   (Π (x_h : (in-hole Φ ((in-hole Θ t_P) (Ξ-apply Φ x))))
+      (hypotheses-loop x_D t_P Φ_1))
+   (where x_h ,(variable-not-in (term (x_D t_P any_0)) 'x-ih))])
+
+;; Returns the inductive hypotheses required for the elimination method of constructor x_ci for
+;; inductive type x_D, when eliminating with motive t_P.
+(define-metafunction tt-ctxtL
+  Δ-constructor-inductive-hypotheses : Δ x x t -> Ξ
+  [(Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P)
+   (hypotheses-loop x_D t_P (Δ-constructor-inductive-telescope Δ x_D x_ci))])
+
+(define-metafunction tt-ctxtL
+  Δ-constructor-method-telescope : Δ x x t -> Ξ
+  [(Δ-constructor-method-telescope Δ x_D x_ci t_P)
+   (Π (x_mi : (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a x_ci)))))
+      hole)
+   (where Θ_p (Δ-constructor-parameters Δ x_D x_ci))
+   (where Ξ_a (Δ-constructor-telescope Δ x_D x_ci))
+   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P))
+   (where x_mi ,(variable-not-in (term (t_P Δ)) 'x-mi))])
+
+;; fold Ξ-compose over map Δ-constructor-method-telescope over the list of constructors
+(define-metafunction tt-ctxtL
+  method-loop : Δ x t (x ...) -> Ξ
+  [(method-loop Δ x_D t_P ()) hole]
+  [(method-loop Δ x_D t_P (x_0 x_rest ...))
+   (Ξ-compose (Δ-constructor-method-telescope Δ x_D x_0 t_P) (method-loop Δ x_D t_P (x_rest ...)))])
+
+;; Returns the telescope of all methods required to eliminate the type x_D with motive t_P
+(define-metafunction tt-ctxtL
+  Δ-methods-telescope : Δ x t -> Ξ
+  [(Δ-methods-telescope Δ x_D t_P)
+   (method-loop Δ x_D t_P (Δ-ref-constructors Δ x_D))])
+
+;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
+;; is in universe U.
+;;
+;; The type of (elim x_D U) is something like:
+;;  (∀ (P : (∀ a -> ... -> (D a ...) -> U))
+;;     (method_ci ...) -> ... ->
+;;     (a -> ... -> (D a ...) ->
+;;       (P a ... (D a ...))))
+;;
+;; x_D   is an inductively defined type
+;; U     is the sort the motive
+;; x_P   is the name of the motive
+;; Ξ_P*D is the telescope of the parameters of x_D and
+;;       the witness of type x_D (applied to the parameters)
+;; Ξ_m   is the telescope of the methods for x_D
+(define-metafunction tt-ctxtL
+  Δ-elim-type : Δ x U -> t
+  [(Δ-elim-type Δ x_D U)
+   (Π (x_P : (in-hole Ξ_P*D U))
+      ;; The methods Ξ_m for each constructor of type x_D
+      (in-hole Ξ_m
+        ;; And finally, the parameters and discriminant
+        (in-hole Ξ_P*D
+          ;; The result is (P a ... (x_D a ...)), i.e., the motive
+          ;; applied to the paramters and discriminant
+          (Ξ-apply Ξ_P*D x_P))))
+   ;; Get the parameters of x_D
+   (where Ξ (Δ-ref-parameter-Ξ Δ x_D))
+   ;; A fresh name to bind the discriminant
+   (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
+   ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
+   ;; of the parameters and the inductive type applied to the
+   ;; parameters
+   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole)))
+   ;; A fresh name for the motive
+   (where x_P ,(variable-not-in (term (Δ Γ x_D Ξ Ξ_P*D x)) 'x-P))
+   ;; The types of the methods for this inductive.
+   (where Ξ_m (Δ-methods-telescope Δ x_D x_P))])
+
+;; TODO: This might belong in the next section, since it's related to evaluation
+;; Generate recursive applications of the eliminator for each inductive argument of type x_D.
+;; In more detaill, given motive t_P, parameters Θ_p, methods Θ_m, and arguments Θ_i to constructor
+;; x_ci for x_D, for each inductively smaller term t_i of type (in-hole Θ_p x_D) inside Θ_i,
+;; generate: (elim x_D U t_P  Θ_m ... Θ_p ... t_i)
+(define-metafunction tt-ctxtL
+  Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (in-hole Θ_i (hole (name t_i (in-hole Θ_r x_ci)))))
+   ((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
+    (in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
+   (side-condition (memq (term x_ci) (term (Δ-ref-constructors Δ x_D))))]
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_nr) hole])
+
+;;; ------------------------------------------------------------------------
+;;; Dynamic semantics
+;;; The majority of this section is dedicated to evaluation of (elim x U), the eliminator for the
+;;; inductively defined type x with a motive whose result is in universe U
+
+(define-extended-language tt-redL tt-ctxtL
+  ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. However,
+  ;; determining whether or not it is partially applied cannot be done with the grammar alone.
+  (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U)))
+  (Θv  ::= hole (Θv v))
+  ;; call-by-value, plus reduce under Π (helps with typing checking)
+  (E   ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)))
+
+(define Θv? (redex-match? tt-redL Θv))
+(define E? (redex-match? tt-redL E))
+(define v? (redex-match? tt-redL v))
+
+(define tt-->
+  (reduction-relation tt-redL
+    (--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2)))
+         (Δ (in-hole E (subst t_1 x t_2)))
+         -->β)
+    (--> (Δ (in-hole E (in-hole Θv ((elim x_D U) v_P))))
+         (Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
+         #|
+          | The elim form must appear applied like so:
+          | (elim x_D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
+          |
+          | Where:
+          |   x_D       is the inductive being eliminated
+          |   U         is the universe of the result of the motive
+          |   v_P       is the motive
+          |   m_{0..n}  are the methods
+          |   p ...     are the parameters of x_D
+          |   c_i       is a constructor of x_d
+          |   a ...     are the arguments to c_i
+          | Unfortunately, Θ contexts turn all this inside out:
+          | TODO: Write better abstractions for this notation
+          |#
+          ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
+          ;; the discriminant: the constructor x_ci applied to its argument Θv_i
+         (where (in-hole (Θv_p (in-hole Θv_i x_ci)) Θv_m) Θv)
+         ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
+         ;; arguments.
+         (side-condition (equal? (term (Θ-length Θv_p)) (term (Ξ-length (Δ-ref-parameter-Ξ Δ x_D)))))
+         ;; Ensure x_ci is actually a constructor for x_D
+         (where (x_c* ...) (Δ-ref-constructors Δ x_D))
+         (side-condition (memq (term x_ci) (term (x_c* ...))))
+         ;; There should be a number of methods equal to the number of constructors; to ensure E
+         ;; doesn't capture methods and Θv_m doesn't capture other arguments
+         (side-condition (equal? (length (term (x_c* ...)))  (term (Θ-length Θv_m))))
+         ;; Find the method for constructor x_ci, relying on the order of the arguments.
+         (where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ x_D x_ci)))
+         ;; Generate the inductive recursion
+         (where Θ_r (Δ-inductive-elim Δ x_D U v_P Θv_p Θv_m Θv_i))
+         -->elim)))
+
+(define-metafunction tt-redL
+  step : Δ e -> e
+  [(step Δ e)
+   e_r
+   (where (_ e_r) ,(car (apply-reduction-relation tt--> (term (Δ e)))))])
+
+(define-metafunction tt-redL
+  reduce : Δ e -> e
+  [(reduce Δ e)
+   e_r
+   (where (_ e_r)
+     ,(let ([r (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)])
+        ;; Efficient check for (= (length r) 1)
+        ;; NB: Check is overly aggressive and produces wrong error,
+        ;; because not reducing under lambda.
+        #;(unless (null? (cdr r))
+          (error "Church-Rosser broken" r))
+        (car r)))])
+
+(define-judgment-form tt-redL
+  #:mode (equivalent I I I)
+  #:contract (equivalent Δ t t)
+
+  [(where t_2 (reduce Δ t_0))
+   (where t_3 (reduce Δ t_1))
+   (side-condition (α-equivalent? t_2 t_3))
+   ----------------- "≡-αβ"
+   (equivalent Δ t_0 t_1)])
+
+;;; ------------------------------------------------------------------------
+;;; Type checking and synthesis
+
+(define-extended-language tt-typingL tt-redL
+  ;; NB: There may be a bijection between Γ and Ξ. That's interesting.
+  ;; NB: Also a bijection between Γ and a list of maps from x to t.
+  (Γ   ::= ∅ (Γ x : t)))
+(define Γ? (redex-match? tt-typingL Γ))
+
+(define-metafunction tt-typingL
+  Γ-union : Γ Γ -> Γ
+  [(Γ-union Γ ∅) Γ]
+  [(Γ-union Γ_2 (Γ_1 x : t))
+   ((Γ-union Γ_2 Γ_1) x : t)])
+
+(define-metafunction tt-typingL
+  Γ-set : Γ x t -> Γ
+  [(Γ-set Γ x t) (Γ x : t)])
+
+;; NB: Depends on clause order
+(define-metafunction tt-typingL
+  Γ-ref : Γ x -> t or #f
+  [(Γ-ref ∅ x) #f]
+  [(Γ-ref (Γ x : t) x) t]
+  [(Γ-ref (Γ x_0 : t_0) x_1) (Γ-ref Γ x_1)])
+
+;; NB: Depends on clause order
+(define-metafunction tt-typingL
+  Γ-remove : Γ x -> Γ
+  [(Γ-remove ∅ x) ∅]
+  [(Γ-remove (Γ x : t) x) Γ]
+  [(Γ-remove (Γ x_0 : t_0) x_1) (Γ-remove Γ x_1)])
+
+(define-metafunction tt-typingL
+  nonpositive : x t -> #t or #f
+  [(nonpositive x (in-hole Θ x))
+   #t]
+  [(nonpositive x (Π (x_0 : (in-hole Θ x)) t))
+   #f]
+  [(nonpositive x (Π (x_0 : t_0) t))
+   ,(and (term (positive x t_0)) (term (nonpositive x t)))]
+  [(nonpositive x t) #t])
+
+(define-metafunction tt-typingL
+  positive : x t -> #t or #f
+  [(positive x (in-hole Θ x))
+   #f]
+  [(positive x (Π (x_0 : (in-hole Θ x)) t))
+   (positive x t)]
+  [(positive x (Π (x_0 : t_0) t))
+   ,(and (term (nonpositive x t_0)) (term (positive x t)))]
+  [(positive x t) #t])
+
+(define-metafunction tt-typingL
+  positive* : x (t ...) -> #t or #f
+  [(positive* x_D ()) #t]
+  [(positive* x_D (t_c t_rest ...))
+   ;; Replace the result of the constructor with (Unv 0), to avoid the result being considered a
+   ;; nonpositive position.
+   ,(and (term (positive x_D (in-hole Ξ (Unv 0)))) (term (positive* x_D (t_rest ...))))
+   (where (in-hole Ξ (in-hole Θ x_D)) t_c)])
+
+;; Holds when the signature Δ and typing context Γ are well-formed.
+(define-judgment-form tt-typingL
+  #:mode (wf I I)
+  #:contract (wf Δ Γ)
+
+  [----------------- "WF-Empty"
+   (wf ∅ ∅)]
+
+  [(type-infer Δ Γ t t_0)
+   (wf Δ Γ)
+   ----------------- "WF-Var"
+   (wf Δ (Γ x : t))]
+
+  [(wf Δ ∅)
+   (type-infer Δ ∅ t_D U_D)
+   (type-infer Δ (∅ x_D : t_D) t_c U_c) ...
+   ;; NB: Ugh this should be possible with pattern matching alone ....
+   (side-condition ,(map (curry equal? (term x_D)) (term (x_D* ...))))
+   (side-condition (positive* x_D (t_c ...)))
+   ----------------- "WF-Inductive"
+   (wf (Δ (x_D : t_D
+               ;; Checks that a constructor for x actually produces an x, i.e., that
+               ;; the constructor is well-formed.
+               ((x_c : (name t_c (in-hole Ξ (in-hole Θ x_D*)))) ...))) ∅)])
+
+;; TODO: Bi-directional and inference?
+;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
+
+;; Holds when e has type t under signature Δ and typing context Γ
+(define-judgment-form tt-typingL
+  #:mode (type-infer I I I O)
+  #:contract (type-infer Δ Γ e t)
+
+  [(wf Δ Γ)
+   (unv-type U_0 U_1)
+   ----------------- "DTR-Unv"
+   (type-infer Δ Γ U_0 U_1)]
+
+  [(where t (Δ-ref-type Δ x))
+   ----------------- "DTR-Inductive"
+   (type-infer Δ Γ x t)]
+
+  [(where t (Γ-ref Γ x))
+   ----------------- "DTR-Start"
+   (type-infer Δ Γ x t)]
+
+  [(type-infer Δ (Γ x : t_0) e t_1)
+   (type-infer Δ Γ (Π (x : t_0) t_1) U)
+   ----------------- "DTR-Abstraction"
+   (type-infer Δ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
+
+  [(type-infer Δ Γ t_0 U_1)
+   (type-infer Δ (Γ x : t_0) t U_2)
+   (unv-pred U_1 U_2 U)
+   ----------------- "DTR-Product"
+   (type-infer Δ Γ (Π (x : t_0) t) U)]
+
+  [(type-infer Δ Γ e_0 t)
+   ;; Cannot rely on type-infer producing normal forms.
+   (where (Π (x_0 : t_0) t_1) (reduce Δ t))
+   (type-check Δ Γ e_1 t_0)
+   (where t_3 (subst t_1 x_0 e_1))
+   ----------------- "DTR-Application"
+   (type-infer Δ Γ (e_0 e_1) t_3)]
+
+  [(where t (Δ-elim-type Δ D U))
+   (type-infer Δ Γ t U_e)
+   ----------------- "DTR-Elim_D"
+   (type-infer Δ Γ (elim D U) t)])
+
+(define-judgment-form tt-typingL
+  #:mode (type-check I I I I)
+  #:contract (type-check Δ Γ e t)
+
+  [(type-infer Δ Γ e t_0)
+   (equivalent Δ t t_0)
+   ----------------- "DTR-Check"
+   (type-check Δ Γ e t)])
diff --git a/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt
similarity index 100%
rename from curnel/redex-lang.rkt
rename to cur-lib/cur/curnel/redex-lang.rkt
diff --git a/lang/reader.rkt b/cur-lib/cur/lang/reader.rkt
similarity index 100%
rename from lang/reader.rkt
rename to cur-lib/cur/lang/reader.rkt
diff --git a/oll.rkt b/cur-lib/cur/oll.rkt
similarity index 80%
rename from oll.rkt
rename to cur-lib/cur/oll.rkt
index 1618cc4..acd8453 100644
--- a/oll.rkt
+++ b/cur-lib/cur/oll.rkt
@@ -12,7 +12,15 @@
   Var
   avar
   var-equal?
-  generate-coq)
+  generate-coq
+
+  ;; private; exported for testing only
+  (for-syntax
+   coq-defns
+   output-latex-bnf
+   output-coq
+   new-name
+   fresh-name))
 
 (begin-for-syntax
   (define-syntax-class dash
@@ -86,27 +94,6 @@
   (define (fresh-name id)
     (datum->syntax id (gensym (syntax->datum id)))))
 
-(module+ test
-  (begin-for-syntax
-    (require rackunit)
-    (define (check-id-equal? v1 v2)
-      (check-equal?
-        (syntax->datum v1)
-        (syntax->datum v2)))
-    (define (check-id-match? v1 v2)
-       (check-regexp-match
-         v1
-         (symbol->string (syntax->datum v2))))
-    (check-id-match?
-      #px"term\\d+"
-      (fresh-name #'term))
-    (check-id-equal?
-      #'stlc-lambda
-      (new-name #'stlc #'lambda))
-    (check-id-match?
-      #px"stlc-term\\d+"
-      (new-name #'stlc (fresh-name #'term)))))
-
 ;; TODO: Oh, this is a mess. Rewrite it.
 (begin-for-syntax
   (define lang-name (make-parameter #'name))
@@ -196,20 +183,7 @@
     (with-output-to-file file-name
       (thunk (printf (output-latex-bnf vars clauses)))
       #:exists 'append)))
-(module+ test
-  (require "stdlib/sugar.rkt")
-  (begin-for-syntax
-    (require rackunit)
-    (check-equal?
-      (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
-        (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
-      (output-latex-bnf #'(x)
-                    #'((term (e) ::= (e1 e2) (lambda (x) e)))))
-    (check-equal?
-      (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
-        (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
-      (output-latex-bnf #'(x)
-                    #'((type (A B C) ::= unit (* A B) (+ A C)))))))
+
 ;; TODO: For better error messages, add context, rename some of these patterns. e.g.
 ;;    (type (meta-vars) ::= ?? )
 ;; TODO: Extend define-language with syntax such as ....
@@ -243,14 +217,6 @@
      (match v2
        [(avar (n2 : Nat))
         (nat-equal? n1 n2)])]))
-(module+ test
-  (require rackunit)
-  (check-equal?
-    (var-equal? (avar z) (avar z))
-    true)
-  (check-equal?
-    (var-equal? (avar z) (avar (s z)))
-    false))
 
 ;; See stlc.rkt for examples
 
@@ -346,41 +312,3 @@
                (format "Eval compute in ~a." body))))
        (displayln (format "~a~a" (coq-defns) output))
        #'(begin))]))
-
-(module+ test
-  (begin-for-syntax
-    (check-equal?
-      (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
-      (format "Inductive nat : Type :=~n| z : nat.~n"))
-    (check-regexp-match
-      "(forall .+ : Type, Type)"
-      (output-coq #'(-> Type Type)))
-    (let ([t (parameterize ([coq-defns ""])
-               (output-coq #'(define-relation (meow gamma term type)
-                               [(g : gamma) (e : term) (t : type)
-                                --------------- T-Bla
-                                (meow g e t)]))
-               (coq-defns))])
-      (check-regexp-match
-        "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
-        (first (string-split t "\n")))
-      (check-regexp-match
-        "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
-        (second (string-split t "\n"))))
-    (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
-                             (lambda* (x : nat) (ih-x : nat) ih-x)
-                             e))])
-      (check-regexp-match
-        "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
-        t))
-    (check-regexp-match
-      "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
-      (parameterize ([coq-defns ""])
-        (output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
-                                              (== nat (plus n m) (plus m n)))))
-        (coq-defns)))
-    (check-regexp-match
-      "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
-      (parameterize ([coq-defns ""])
-        (output-coq #'(define (add1 (n : nat)) (s n)))
-        (coq-defns)))))
diff --git a/cur-lib/cur/stdlib/bool.rkt b/cur-lib/cur/stdlib/bool.rkt
new file mode 100644
index 0000000..df131b2
--- /dev/null
+++ b/cur-lib/cur/stdlib/bool.rkt
@@ -0,0 +1,24 @@
+#lang s-exp "../cur.rkt"
+(require "sugar.rkt")
+(provide Bool true false if not and or)
+
+(data Bool : Type
+  (true : Bool)
+  (false : Bool))
+
+(define-syntax-rule (if t s f)
+  (match t
+    [true s]
+    [false f]))
+
+(define (not (x : Bool)) (if x false true))
+
+(define (and (x : Bool) (y : Bool))
+  (if x
+      y
+      (not y)))
+
+(define (or (x : Bool) (y : Bool))
+  (if x
+      true
+      y))
diff --git a/cur-lib/cur/stdlib/maybe.rkt b/cur-lib/cur/stdlib/maybe.rkt
new file mode 100644
index 0000000..6ebe99b
--- /dev/null
+++ b/cur-lib/cur/stdlib/maybe.rkt
@@ -0,0 +1,13 @@
+#lang s-exp "../cur.rkt"
+(require "sugar.rkt")
+(provide Maybe none some some/i)
+
+(data Maybe : (forall (A : Type) Type)
+  (none : (forall (A : Type) (Maybe A)))
+  (some : (forall* (A : Type) (a : A) (Maybe A))))
+
+(define-syntax (some/i syn)
+  (syntax-case syn ()
+   [(_ a)
+    (let ([a-ty (type-infer/syn #'a)])
+      #`(some #,a-ty a))]))
diff --git a/stdlib/nat.rkt b/cur-lib/cur/stdlib/nat.rkt
similarity index 55%
rename from stdlib/nat.rkt
rename to cur-lib/cur/stdlib/nat.rkt
index 871c39a..435cc8c 100644
--- a/stdlib/nat.rkt
+++ b/cur-lib/cur/stdlib/nat.rkt
@@ -3,55 +3,37 @@
 ;; TODO: override (all-defined-out) to enable exporting all these
 ;; properly.
 (provide Nat z s add1 sub1 plus mult exp square nat-equal? even? odd?)
-(module+ test
-  (require rackunit))
 
 (data Nat : Type
   (z : Nat)
   (s : (-> Nat Nat)))
 
 (define (add1 (n : Nat)) (s n))
-(module+ test
-  (check-equal? (add1 (s z)) (s (s z))))
 
 (define (sub1 (n : Nat))
   (match n
     [z z]
     [(s (x : Nat)) x]))
-(module+ test
-  (check-equal? (sub1 (s z)) z))
 
 (define (plus (n1 : Nat) (n2 : Nat))
   (match n1
     [z n2]
     [(s (x : Nat))
      (s (recur x))]))
-(module+ test
-  (check-equal? (plus z z) z)
-  (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
 
 (define (mult (m : Nat) (n : Nat))
   (match m
     [z z]
     [(s (x : Nat))
      (plus n (recur x))]))
-(module+ test
-  (check-equal? (mult (s (s z)) z) z)
-  (check-equal? (mult (s (s z)) (s z)) (s (s z))))
 
 (define (exp (m : Nat) (e : Nat))
   (match m
     [z (s z)]
     [(s (x : Nat))
      (mult e (recur x))]))
-(module+ test
-  #;(check-equal? (exp z z) (s z))
-  #;(check-equal? (exp (s z) z) z))
 
 (define square (run (exp (s (s z)))))
-;; TODO: This test takes too long t run
-#;(module+ test
-  (check-equal? (square (s (s z))) (s (s (s (s z))))))
 
 ;; Credit to this function goes to Max
 (define nat-equal?
@@ -64,10 +46,6 @@
             false
             (lambda* (x : Nat) (ih-bla : Bool)
                      (ih x))))))
-(module+ test
-  (check-equal? (nat-equal? z z) true)
-  (check-equal? (nat-equal? z (s z)) false)
-  (check-equal? (nat-equal? (s z) (s z)) true))
 
 (define (even? (n : Nat))
   (match n
@@ -77,26 +55,3 @@
 
 (define (odd? (n : Nat))
   (not (even? n)))
-
-(module+ test
-  (check-equal?
-    (even? z)
-    true)
-  (check-equal?
-    (even? (s z))
-    false)
-  (check-equal?
-    (even? (s (s z)))
-    true)
-  (check-equal?
-    (odd? z)
-    false)
-  (check-equal?
-    (odd? (s z))
-    true)
-  (check-equal?
-    (odd? (s (s z)))
-    false)
-  #;(check-equal?
-    (odd? (s (s (s z))))
-    true))
diff --git a/stdlib/prop.rkt b/cur-lib/cur/stdlib/prop.rkt
similarity index 75%
rename from stdlib/prop.rkt
rename to cur-lib/cur/stdlib/prop.rkt
index 81e05a6..ad4371a 100644
--- a/stdlib/prop.rkt
+++ b/cur-lib/cur/stdlib/prop.rkt
@@ -15,17 +15,11 @@
   thm:proj2 pf:proj2
   == refl)
 
-(module+ test
-  (require rackunit))
-
 (data True : Type (T : True))
 
 (define thm:anything-implies-true (forall (P : Type) True))
 (define pf:anything-implies-true (lambda (P : Type) T))
 
-(module+ test
-  (:: pf:anything-implies-true thm:anything-implies-true))
-
 (data False : Type)
 
 (define-type (Not (A : Type)) (-> A False))
@@ -51,9 +45,6 @@
          (And Q P))
       ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
 
-(module+ test
-  (:: pf:and-is-symmetric thm:and-is-symmetric))
-
 (define thm:proj1
   (forall* (A : Type) (B : Type) (c : (And A B)) A))
 
@@ -63,9 +54,6 @@
       (lambda* (A : Type) (B : Type) (c : (And A B)) A)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
-(module+ test
-  (:: pf:proj1 thm:proj1))
-
 (define thm:proj2
   (forall* (A : Type) (B : Type) (c : (And A B)) B))
 
@@ -75,9 +63,6 @@
       (lambda* (A : Type) (B : Type) (c : (And A B)) B)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
-(module+ test
-  (:: pf:proj2 thm:proj2))
-
 #| TODO: Disabled until #22 fixed
 (data Or : (forall* (A : Type) (B : Type) Type)
   (left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
@@ -100,30 +85,3 @@
 
 (data == : (forall* (A : Type) (x : A) (-> A Type))
   (refl : (forall* (A : Type) (x : A) (== A x x))))
-
-(module+ test
-  (require  "bool.rkt" "nat.rkt")
-  (check-equal?
-    (elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
-         (λ* (A : Type) (x : A) z)
-         Bool
-         true
-         true
-         (refl Bool true))
-    z)
-
-  (check-equal?
-    (conj/i (conj/i T T) T)
-    (conj (And True True) True (conj True True T T) T))
-
-  (define (id (A : Type) (x : A)) x)
-
-  (check-equal?
-    ((id (== True T T))
-     (refl True (run (id True T))))
-    (refl True T))
-
-  (check-equal?
-    ((id (== True T T))
-     (refl True (id True T)))
-    (refl True T)))
diff --git a/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt
similarity index 87%
rename from stdlib/sugar.rkt
rename to cur-lib/cur/stdlib/sugar.rkt
index 6f8eeaa..3e41b8c 100644
--- a/stdlib/sugar.rkt
+++ b/cur-lib/cur/stdlib/sugar.rkt
@@ -249,53 +249,3 @@
        (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
        ;; Void is undocumented and a hack, but sort of works
        #'(void))]))
-
-(module+ test
-  (require rackunit (submod ".."))
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type)
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type)
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type)
-
-  (check-equal?
-    (let ([x Type]
-          [y (λ (x : (Type 1)) x)])
-      (y x))
-    Type)
-
-  (check-equal?
-    (let ([(x : (Type 1)) Type]
-          [y (λ (x : (Type 1)) x)])
-      (y x))
-    Type)
-
-  ;; check that raises decent syntax error
-  ;; Can't use this because (lambda () ...) and thunk are not things in Cur at runtime
-  #;(check-exn
-    exn:fail:syntax?
-    (let ([x : (Type 1) Type]
-          [y (λ (x : (Type 1)) x)])
-      (y x)))
-
-  ;; check that raises type error
-  #;(check-exn
-    exn:fail:syntax?
-    (let ([x uninferrable-expr]
-          [y (λ (x : (Type 1)) x)])
-      (y x)))
-
-  )
diff --git a/stdlib/tactics/base.rkt b/cur-lib/cur/stdlib/tactics/base.rkt
similarity index 100%
rename from stdlib/tactics/base.rkt
rename to cur-lib/cur/stdlib/tactics/base.rkt
diff --git a/stdlib/tactics/sartactics.rkt b/cur-lib/cur/stdlib/tactics/sartactics.rkt
similarity index 96%
rename from stdlib/tactics/sartactics.rkt
rename to cur-lib/cur/stdlib/tactics/sartactics.rkt
index 7a53e06..5243130 100644
--- a/stdlib/tactics/sartactics.rkt
+++ b/cur-lib/cur/stdlib/tactics/sartactics.rkt
@@ -124,11 +124,3 @@
             (loop (apply (lookup-tactic #'tactic)
                     (append (syntax->list #'(arg ...)) (list ps)))
                   (cons cmd cmds)))]))))
-
-(module+ test
-  (require
-    rackunit
-    "../bool.rkt")
-  (define-theorem meow (forall (x : Bool) Bool))
-  #;(proof (interactive))
-  )
diff --git a/stdlib/tactics/standard.rkt b/cur-lib/cur/stdlib/tactics/standard.rkt
similarity index 82%
rename from stdlib/tactics/standard.rkt
rename to cur-lib/cur/stdlib/tactics/standard.rkt
index d2b83df..0c1831b 100644
--- a/stdlib/tactics/standard.rkt
+++ b/cur-lib/cur/stdlib/tactics/standard.rkt
@@ -98,31 +98,3 @@
 ;; Open interactive REPL for tactic DSL; exit with QED command, which
 ;; returns a QED script
 ;(define-syntax interactive-proof)
-
-(module+ test
-  (require
-    rackunit
-    "../bool.rkt")
-  (define-theorem meow (forall (x : Bool) Bool))
-  (proof
-    (intro x)
-    (by-assumption))
-  (define-theorem meow1 (forall (x : Bool) Bool))
-  (proof
-    (obvious)
-    ;; TODO: Add ability to check output
-    #;(print))
-  (define-theorem meow2 (forall (x : Bool) Bool))
-  (proof
-    (intro x)
-    (restart)
-    (intro x)
-    (by-assumption))
-  (define-theorem meow3 (forall (x : Bool) Bool))
-  (proof (obvious))
-  ;; TODO: Fix this unit test so it doesn't require interaction
-  (define-theorem meow4 (forall (x : Bool) Bool))
-  #;(proof (interactive))
-  ;; TODO: Add check-cur-equal? for unit testing?
-  #;(check-pred (curry cur-equal? '(lambda (x : bool) x)))
-  )
diff --git a/stdlib/typeclass.rkt b/cur-lib/cur/stdlib/typeclass.rkt
similarity index 85%
rename from stdlib/typeclass.rkt
rename to cur-lib/cur/stdlib/typeclass.rkt
index bc41256..8ce6373 100644
--- a/stdlib/typeclass.rkt
+++ b/cur-lib/cur/stdlib/typeclass.rkt
@@ -71,27 +71,3 @@
                     #'body))
                 #`(define #,(format-id syn "~a-~a" name #'param)
                     #,body))))]))
-
-(module+ test
-  (require rackunit)
-  (typeclass (Eqv (A : Type))
-    (equal? : (forall* (a : A) (b : A) Bool)))
-  (impl (Eqv Bool)
-    (define (equal? (a : Bool) (b : Bool))
-      (if a
-          (if b true false)
-          (if b false true))))
-  (impl (Eqv Nat)
-    (define equal? nat-equal?))
-  (check-equal?
-    (equal? z z)
-    true)
-  (check-equal?
-    (equal? z (s z))
-    false)
-  (check-equal?
-    (equal? true false)
-    false)
-  (check-equal?
-    (equal? true true)
-    true))
diff --git a/cur-lib/info.rkt b/cur-lib/info.rkt
new file mode 100644
index 0000000..fc2d01e
--- /dev/null
+++ b/cur-lib/info.rkt
@@ -0,0 +1,7 @@
+#lang info
+(define collection 'multi)
+(define deps '("base" ("redex-lib" #:version "1.11")))
+(define build-deps '())
+(define pkg-desc "implementation (no documentation, tests) part of \"cur\".")
+(define version "0.2")
+(define pkg-authors '(wilbowma))
diff --git a/cur-test/cur/tests/oll.rkt b/cur-test/cur/tests/oll.rkt
new file mode 100644
index 0000000..04188eb
--- /dev/null
+++ b/cur-test/cur/tests/oll.rkt
@@ -0,0 +1,85 @@
+#lang cur
+
+;; NB TODO: raco test reports incorrect number of total tests due to
+;; beign-for-syntax; but all failing tests correctly raise errors
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/oll)
+
+(begin-for-syntax
+  (require rackunit)
+  (define (check-id-equal? v1 v2)
+    (check-equal?
+     (syntax->datum v1)
+     (syntax->datum v2)))
+  (define (check-id-match? v1 v2)
+    (check-regexp-match
+     v1
+     (symbol->string (syntax->datum v2))))
+  (check-id-match?
+   #px"term\\d+"
+   (fresh-name #'term))
+  (check-id-equal?
+   #'stlc-lambda
+   (new-name #'stlc #'lambda))
+  (check-id-match?
+   #px"stlc-term\\d+"
+   (new-name #'stlc (fresh-name #'term))))
+
+(begin-for-syntax
+  (check-equal?
+   (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
+           (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
+   (output-latex-bnf #'(x)
+                     #'((term (e) ::= (e1 e2) (lambda (x) e)))))
+  (check-equal?
+   (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
+           (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
+   (output-latex-bnf #'(x)
+                     #'((type (A B C) ::= unit (* A B) (+ A C))))))
+
+(check-equal?
+ (var-equal? (avar z) (avar z))
+ true)
+(check-equal?
+ (var-equal? (avar z) (avar (s z)))
+ false)
+
+(begin-for-syntax
+  (check-equal?
+   (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
+   (format "Inductive nat : Type :=~n| z : nat.~n"))
+  (check-regexp-match
+   "(forall .+ : Type, Type)"
+   (output-coq #'(-> Type Type)))
+  (let ([t (parameterize ([coq-defns ""])
+             (output-coq #'(define-relation (meow gamma term type)
+                             [(g : gamma) (e : term) (t : type)
+                              --------------- T-Bla
+                              (meow g e t)]))
+             (coq-defns))])
+    (check-regexp-match
+     "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
+     (first (string-split t "\n")))
+    (check-regexp-match
+     "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
+     (second (string-split t "\n"))))
+  (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
+                               (lambda* (x : nat) (ih-x : nat) ih-x)
+                               e))])
+    (check-regexp-match
+     "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
+     t))
+  (check-regexp-match
+   "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
+   (parameterize ([coq-defns ""])
+     (output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
+                                                      (== nat (plus n m) (plus m n)))))
+     (coq-defns)))
+  (check-regexp-match
+   "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
+   (parameterize ([coq-defns ""])
+     (output-coq #'(define (add1 (n : nat)) (s n)))
+     (coq-defns))))
diff --git a/cur-test/cur/tests/redex-core.rkt b/cur-test/cur/tests/redex-core.rkt
new file mode 100644
index 0000000..eb2da16
--- /dev/null
+++ b/cur-test/cur/tests/redex-core.rkt
@@ -0,0 +1,658 @@
+#lang racket/base
+(require
+ redex/reduction-semantics
+ cur/curnel/redex-core
+ rackunit
+ racket/function
+ (only-in racket/set set=?))
+(define-syntax-rule (check-holds (e ...))
+  (check-true
+   (judgment-holds (e ...))))
+(define-syntax-rule (check-not-holds (e ...))
+  (check-false
+   (judgment-holds (e ...))))
+(define-syntax-rule (check-equiv? e1 e2)
+  (check (default-equiv) e1 e2))
+(define-syntax-rule (check-not-equiv? e1 e2)
+  (check (compose not (default-equiv)) e1 e2))
+
+(default-equiv (lambda (x y) (term (α-equivalent? ,x ,y))))
+
+;; Syntax tests
+;; ------------------------------------------------------------------------
+
+(define-term Type (Unv 0))
+(check-true (x? (term T)))
+(check-true (x? (term A)))
+(check-true (x? (term truth)))
+(check-true (x? (term zero)))
+(check-true (x? (term s)))
+(check-true (t? (term zero)))
+(check-true (t? (term s)))
+(check-true (x? (term nat)))
+(check-true (t? (term nat)))
+(check-true (t? (term A)))
+(check-true (t? (term S)))
+(check-true (U? (term (Unv 0))))
+(check-true (U? (term Type)))
+(check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
+
+;; TODO: Rename these signatures, and use them in all future tests.
+(define Δ (term ((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat)))))
+                 (bool : (Unv 0) ((true : bool) (false : bool))))))
+(define Δ0 (term ∅))
+(define Δ3 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ()))))
+(define Δ4 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                         ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))))))
+(check-true (Δ? Δ0))
+(check-true (Δ? Δ))
+(check-true (Δ? Δ4))
+(check-true (Δ? Δ3))
+(check-true (Δ? Δ4))
+(define sigma (term ((((((∅ (true : (Unv 0) ((T : true))))
+                         (false : (Unv 0) ()))
+                        (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                               ()))
+                       (nat : (Unv 0) ()))
+                      (heap : (Unv 0) ()))
+                     (pre : (Π (temp808 : heap) (Unv 0)) ()))))
+(check-true (Δ? (term (∅ (true : (Unv 0) ((T : true)))))))
+(check-true (Δ? (term (∅ (false : (Unv 0) ())))))
+(check-true (Δ? (term (∅ (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                                ())))))
+(check-true (Δ? (term (∅ (nat : (Unv 0) ())))))
+(check-true (Δ? (term (∅ (pre : (Π (temp808 : heap) (Unv 0)) ())))))
+
+(check-true (Δ? (term ((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ())))))
+(check-true (Δ? (term (((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ()))
+                       (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                              ())))))
+(check-true (Δ? sigma))
+(check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
+
+
+;; α-equiv and subst tests
+;; ------------------------------------------------------------------------
+(check-true
+ (term
+  (α-equivalent?
+   (Π (a : S) (Π (b : B) ((and S) B)))
+   (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
+
+;; Various accessor tests
+;; ------------------------------------------------------------------------
+
+(check-equal?
+ (term (Δ-key-by-constructor ,Δ zero))
+ (term nat))
+(check-equal?
+ (term (Δ-key-by-constructor ,Δ s))
+ (term nat))
+
+(check-equal?
+ (term (Δ-ref-constructor-map ,Δ nat))
+ (term ((zero : nat) (s : (Π (x : nat) nat)))))
+(check-equal?
+ (term (Δ-ref-constructor-map ,sigma false))
+ (term ()))
+
+;; Telescope tests
+;; ------------------------------------------------------------------------
+;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed
+(define (telescope-equiv x y)
+  (alpha-equivalent? ttL (term (in-hole ,x (Unv 0))) (term (in-hole ,y (Unv 0)))))
+(define-syntax-rule (check-telescope-equiv? e1 e2)
+  (check telescope-equiv e1 e2))
+(define-syntax-rule (check-telescope-not-equiv? e1 e2)
+  (check (compose not telescope-equiv) e1 e2))
+
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ nat))
+ (term hole))
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ4 and))
+ (term (Π (A : Type) (Π (B : Type) hole))))
+
+(check-telescope-equiv?
+ (term (Ξ-compose
+        (Π (x : t_0) (Π (y : t_1) hole))
+        (Π (z : t_2) (Π (a : t_3) hole))))
+ (term (Π (x : t_0) (Π (y : t_1) (Π (z : t_2) (Π (a : t_3) hole))))))
+
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ nat (λ (x : nat) nat)))
+ (term (Π (m-zero : ((λ (x : nat) nat) zero))
+          (Π (m-s : (Π (x : nat) (Π (x-ih : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x))))) hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ nat P))
+ (term (Π (m-zero : (P zero))
+          (Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x)))))
+             hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ  nat (λ (x : nat) nat)))
+ (term (Π (m-zero :  ((λ (x : nat) nat) zero))
+          (Π (m-s : (Π (x : nat) (Π (ih-x : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x)))))
+             hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ4 and (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))))
+ (term (Π (m-conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B)
+                                                              ((((λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+                                                                 A)
+                                                                B)
+                                                               ((((conj A) B) a) b)))))))
+          hole)))
+(check-true (x? (term false)))
+(check-true (Ξ? (term hole)))
+(check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
+(check-true (redex-match? ttL ((x : t) ...) (term ())))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x))))
+ (term hole))
+
+;; Tests for inductive elimination
+;; ------------------------------------------------------------------------
+;; TODO: Insufficient tests, no tests of inductives with parameters, or complex induction.
+(check-true
+ (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
+(check-telescope-equiv?
+ (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
+                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                         (hole zero)))
+ (term (hole (((((elim nat Type) (λ (x : nat) nat))
+                (s zero))
+               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              zero))))
+(check-telescope-equiv?
+ (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
+                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                         (hole (s zero))))
+ (term (hole (((((elim nat Type) (λ (x : nat) nat))
+                (s zero))
+               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              (s zero)))))
+
+;; Tests for dynamic semantics
+;; ------------------------------------------------------------------------
+
+(check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (v? (term (refl Nat))))
+(check-true (v? (term ((refl Nat) z))))
+
+;; TODO: Move equivalence up here, and use in these tests.
+(check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
+(check-equiv? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
+(check-not-equiv? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
+(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
+                  (term (Π (x : t) (Unv 0))))
+(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
+                  (term (Π (x : t) (x x))))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat)
+                                                (s (s x)))))
+                                zero)))
+              (term (s zero)))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat)
+                                                (s (s x)))))
+                                (s zero))))
+              (term (s (s zero))))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                (s (s (s zero))))))
+              (term (s (s (s (s zero))))))
+
+(check-equiv?
+ (term (reduce ,Δ
+               (((((elim nat Type) (λ (x : nat) nat))
+                  (s (s zero)))
+                 (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                (s (s zero)))))
+ (term (s (s (s (s zero))))))
+(check-equiv?
+ (term (step ,Δ
+             (((((elim nat Type) (λ (x : nat) nat))
+                (s (s zero)))
+               (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+              (s (s zero)))))
+ (term
+  (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+    (s zero))
+   (((((elim nat Type) (λ (x : nat) nat))
+      (s (s zero)))
+     (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+    (s zero)))))
+(check-equiv?
+ (term (step ,Δ (step ,Δ
+                      (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+                        (s zero))
+                       (((((elim nat Type) (λ (x : nat) nat))
+                          (s (s zero)))
+                         (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                        (s zero))))))
+ (term
+  ((λ (ih-x1 : nat) (s ih-x1))
+   (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+     zero)
+    (((((elim nat Type) (λ (x : nat) nat))
+       (s (s zero)))
+      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+     zero)))))
+
+(define-syntax-rule (check-equivalent e1 e2)
+  (check-holds (equivalent ∅ e1 e2)))
+(check-equivalent
+ (λ (x : Type) x) (λ (y : Type) y))
+(check-equivalent
+ (Π (x : Type) x) (Π (y : Type) y))
+
+;; Test static semantics
+;; ------------------------------------------------------------------------
+
+(check-true (term (positive* nat (nat))))
+(check-true (term (positive* nat ((Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))))
+(check-true (term (positive* nat ((Π (x : nat) nat)))))
+;; (nat -> nat) -> nat
+;; Not sure if this is actually supposed to pass
+(check-false (term (positive* nat ((Π (x : (Π (y : nat) nat)) nat)))))
+;; ((Unv 0) -> nat) -> nat
+(check-true (term (positive* nat ((Π (x : (Π (y : (Unv 0)) nat)) nat)))))
+;; (((nat -> (Unv 0)) -> nat) -> nat)
+(check-true (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))))
+;; Not sure if this is actually supposed to pass
+;; ((nat -> nat) -> nat) -> nat
+(check-false (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat)))))
+
+(check-true (judgment-holds (wf ,Δ0 ∅)))
+(check-true (redex-match? tt-redL (in-hole Ξ (Unv 0)) (term (Unv 0))))
+(check-true (redex-match? tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
+                          (term (Π (x : nat) nat))))
+(define (bindings-equal? l1 l2)
+  (map set=? l1 l2))
+(check-pred
+ (curry bindings-equal?
+        (list (list
+               (make-bind 'Ξ (term (Π (x : nat) hole)))
+               (make-bind 'Φ (term hole))
+               (make-bind 'Θ (term hole)))
+              (list
+               (make-bind 'Ξ (term hole))
+               (make-bind 'Φ (term (Π (x : nat) hole)))
+               (make-bind 'Θ (term hole)))))
+ (map match-bindings (redex-match tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
+                                  (term (Π (x : nat) nat)))))
+(check-pred
+ (curry bindings-equal?
+        (list
+         (list
+          (make-bind 'Φ (term (Π (x : nat) hole)))
+          (make-bind 'Θ (term hole)))))
+ (map match-bindings (redex-match tt-redL (in-hole hole (in-hole Φ (in-hole Θ nat)))
+                                  (term (Π (x : nat) nat)))))
+
+(check-true
+ (redex-match? tt-redL
+               (in-hole hole (in-hole hole (in-hole hole nat)))
+               (term nat)))
+(check-true
+ (redex-match? tt-redL
+               (in-hole hole (in-hole (Π (x : nat) hole) (in-hole hole nat)))
+               (term (Π (x : nat) nat))))
+(check-holds (wf (∅ (nat : (Unv 0) ())) ∅))
+
+(check-holds (wf ,Δ0 ∅))
+(check-holds (type-infer ∅ ∅ (Unv 0) U))
+(check-holds (type-infer ∅ (∅ nat : (Unv 0)) nat U))
+(check-holds (type-infer ∅ (∅ nat : (Unv 0)) (Π (x : nat) nat) U))
+(check-true (term (positive* nat (nat (Π (x : nat) nat)))))
+(check-holds
+ (wf (∅ (nat : (Unv 0) ((zero : nat)))) ∅))
+(check-holds
+ (wf (∅ (nat : (Unv 0) ((s : (Π (x : nat) nat))))) ∅))
+(check-holds (wf ,Δ ∅))
+
+(check-holds (wf ,Δ3 ∅))
+(check-holds (wf ,Δ4 ∅))
+(check-holds (wf (∅ (truth : (Unv 0) ())) ∅))
+(check-holds (wf ∅ (∅ x : (Unv 0))))
+(check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : nat)))
+(check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : (Π (x : nat) nat))))
+
+(check-holds (type-infer ∅ ∅ (Unv 0) (Unv 1)))
+(check-holds (type-infer ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1)))
+(check-holds (type-infer ∅ (∅ x : (Unv 0)) x (Unv 0)))
+(check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
+                           (Π (x_3 : x_0) x_1) (Unv 0)))
+(check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) x_0 U_1))
+(check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2))
+(check-holds (unv-pred (Unv 0) (Unv 0) (Unv 0)))
+(check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t))
+
+(check-holds (type-check ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))
+(check-holds (type-check ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
+                             (Π (y : (Unv 0)) (Π (x : y) y))))
+
+(check-equal? (list (term (Unv 1)))
+              (judgment-holds
+               (type-infer ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))
+                             U)
+               U))
+;; ---- Elim
+;; TODO: Clean up/Reorganize these tests
+(check-true
+ (redex-match? tt-typingL
+               (in-hole Θ_m (((elim x_D U) e_D) e_P))
+               (term ((((elim truth Type) T) (Π (x : truth) (Unv 1))) (Unv 0)))))
+(define Δtruth (term (∅ (truth : (Unv 0) ((T : truth))))))
+(check-holds (type-infer ,Δtruth ∅ truth (in-hole Ξ U)))
+(check-holds (type-infer ,Δtruth ∅ T (in-hole Θ_ai truth)))
+(check-holds (type-infer ,Δtruth ∅ (λ (x : truth) (Unv 1))
+                         (in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
+
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
+ (term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole)))
+(check-holds (type-infer ,Δtruth ∅ (elim truth Type) t))
+(check-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
+                         ∅
+                         ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
+                          T)
+                         (Unv 1)))
+(check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
+                             ∅
+                             ((((elim truth (Unv 1)) Type) Type) T)
+                             (Unv 1)))
+(check-holds
+ (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
+(check-holds
+ (type-infer ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))))
+               t))
+(check-holds
+ (type-infer ,Δ ∅ nat (in-hole Ξ U)))
+(check-holds
+ (type-infer ,Δ ∅ zero (in-hole Θ_ai nat)))
+(check-holds
+ (type-infer ,Δ ∅ (λ (x : nat) nat)
+             (in-hole Ξ (Π (x : (in-hole Θ nat)) U))))
+(define-syntax-rule (nat-test syn ...)
+  (check-holds (type-check ,Δ syn ...)))
+(nat-test ∅ (Π (x : nat) nat) (Unv 0))
+(nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
+(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero)
+              (λ (x : nat) (λ (ih-x : nat) x))) zero)
+            nat)
+(nat-test ∅ nat (Unv 0))
+(nat-test ∅ zero nat)
+(nat-test ∅ s (Π (x : nat) nat))
+(nat-test ∅ (s zero) nat)
+;; TODO: Meta-function auto-currying and such
+(check-holds
+ (type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat))
+                    zero)
+                   (λ (x : nat) (λ (ih-x : nat) x)))
+             t))
+(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
+               zero)
+              (λ (x : nat) (λ (ih-x : nat) x)))
+             zero)
+            nat)
+(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
+               (s zero))
+              (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+             zero)
+            nat)
+(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat))
+               (s zero))
+              (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
+            nat)
+(nat-test (∅ n : nat)
+          (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n)
+          nat)
+(check-holds
+ (type-check (,Δ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
+             (∅ n2 : nat)
+             (((((elim nat (Unv 0)) (λ (x : nat) bool))
+                btrue)
+               (λ (x : nat) (λ (ih-x : bool) bfalse)))
+              n2)
+             bool))
+(check-not-holds
+ (type-check ,Δ ∅
+             ((((elim nat (Unv 0)) nat) (s zero)) zero)
+             nat))
+(define lam (term (λ (nat : (Unv 0)) nat)))
+(check-equivalent
+ (Π (nat : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer ,Δ0 ∅ ,lam t) t)))
+(check-equivalent
+ (Π (nat : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer ,Δ ∅ ,lam t) t)))
+(check-equivalent
+ (Π (x : (Π (y : (Unv 0)) y)) nat)
+ ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
+                                   t) t)))
+(check-equivalent
+ (Π (y : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (y : (Unv 0)) y) t) t)))
+(check-equivalent
+ (Unv 0)
+ ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅
+                                   ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
+                                    (λ (y : (Unv 0)) y))
+                                   t) t)))
+(check-equal?
+ (list (term (Unv 0)) (term (Unv 1)))
+ (judgment-holds
+  (type-infer ,Δ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))
+              U) U))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0))
+             conj (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : P) (Π (y : Q) ((and P) Q)))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) S (Unv 0)))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
+             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
+             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
+(check-holds
+ (type-check ,Δ4 ∅ (λ (S : (Unv 0)) (conj S))
+             (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
+(check-holds
+ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((conj true) true) tt) tt)
+             ((and true) true)))
+(check-holds
+ (type-infer ,Δ4 ∅ and (in-hole Ξ U_D)))
+(check-holds
+ (type-infer (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((conj true) true) tt) tt)
+             (in-hole Θ and)))
+(check-holds
+ (type-infer (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+             (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
+(check-holds
+ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((((elim and (Unv 0))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                true))))
+                 (λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) tt)))))
+                true) true)
+              ((((conj true) true) tt) tt))
+             true))
+(check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
+(check-holds
+ (type-infer ,Δ4 ∅ and (in-hole Ξ U)))
+(check-holds
+ (type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
+             ab (in-hole Θ and)))
+(check-true
+ (redex-match? tt-redL
+               (in-hole Ξ (Π (x : (in-hole Θ and)) U))
+               (term (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0)))))))
+(check-holds
+ (type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                           ((and B) A))))
+             (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
+(check-holds
+ (equivalent ,Δ4
+             (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))
+             (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0))))))
+(check-holds
+ (type-infer ,Δ4 ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                           ((and B) A))))
+             (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
+(check-holds
+ (type-check ,Δ4
+             (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
+             ((((((elim and (Unv 0))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                ((and B) A)))))
+                 (λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) ((((conj B) A) b) a))))))
+                P) Q) ab)
+             ((and Q) P)))
+(check-holds
+ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) ((and B) A))))
+             (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))))
+(check-holds
+ (type-infer (,Δ4 (true : (Unv 0) ((tt : true))))
+             ((∅ A : Type) B : Type)
+             (conj B)
+             t))
+(check-holds
+ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((((elim and (Unv 0))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                ((and B) A)))))
+                 (λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) ((((conj B) A) b) a))))))
+                true) true)
+              ((((conj true) true) tt) tt))
+             ((and true) true)))
+(define gamma (term (∅ temp863 : pre)))
+(check-holds (wf ,sigma ∅))
+(check-holds (wf ,sigma ,gamma))
+(check-holds
+ (type-infer ,sigma ,gamma (Unv 0) t))
+(check-holds
+ (type-infer ,sigma ,gamma pre t))
+(check-holds
+ (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
+(check-holds
+ (type-infer ,sigma ,gamma pre t))
+(check-holds
+ (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) false (in-hole Ξ U_D)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) x (in-hole Θ false)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
+             (in-hole Ξ (Π (x : (in-hole Θ false)) U))))
+(check-true
+ (redex-match? tt-typingL
+               ((in-hole Θ_m ((elim x_D U) e_P)) e_D)
+               (term (((elim false (Unv 1)) (λ (y : false) (Π (x : Type) x)))
+                      x))))
+(check-holds
+ (type-check ,sigma (,gamma x : false)
+             (((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x)
+             (Π (x : (Unv 0)) x)))
+
+;; nat-equal? tests
+(define zero?
+  (term ((((elim nat Type) (λ (x : nat) bool))
+          true)
+         (λ (x : nat) (λ (x_ih : bool) false)))))
+(check-holds
+ (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
+(check-equal?
+ (term (reduce ,Δ (,zero? zero)))
+ (term true))
+(check-equal?
+ (term (reduce ,Δ (,zero? (s zero))))
+ (term false))
+(define ih-equal?
+  (term ((((elim nat Type) (λ (x : nat) bool))
+          false)
+         (λ (x : nat) (λ (y : bool) (x_ih x))))))
+(check-holds
+ (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
+             ,ih-equal?
+             (Π (x : nat) bool)))
+(check-holds
+ (type-infer ,Δ ∅ nat (Unv 0)))
+(check-holds
+ (type-infer ,Δ ∅ bool (Unv 0)))
+(check-holds
+ (type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
+(define nat-equal?
+  (term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool)))
+          ,zero?)
+         (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+                        ,ih-equal?)))))
+(check-holds
+ (type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
+             ((nat-equal? zero) zero)
+             bool))
+(check-holds
+ (type-check ,Δ ∅
+             ,nat-equal?
+             (Π (x : nat) (Π (y : nat) bool))))
+(check-equal?
+ (term (reduce ,Δ ((,nat-equal? zero) (s zero))))
+ (term false))
+(check-equal?
+ (term (reduce ,Δ ((,nat-equal? (s zero)) zero)))
+ (term false))
+
+;; == tests
+(define Δ= (term (,Δ (== : (Π (A : (Unv 0)) (Π (a : A) (Π (b : A) (Unv 0))))
+                         ((refl : (Π (A : (Unv 0)) (Π (a : A) (((== A) a) a)))))))))
+(check-true (Δ? Δ=))
+
+(define refl-elim
+  (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
+                                                                                        A1)
+                                                                                       x1)
+                                                                                      y1))
+                                                                              nat)))))
+             (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))
+(check-holds
+ (type-check ,Δ= ∅ ,refl-elim nat))
+(check-true
+ (redex-match?
+  tt-redL
+  (Δ (in-hole E (in-hole Θ ((elim x_D U) e_P))))
+  (term (,Δ= ,refl-elim))))
+(check-true
+ (redex-match?
+  tt-redL
+  (in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m)
+  (term (((((hole
+             (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true)))))
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ= ==))
+ (term (Π (A : Type) (Π (a : A) (Π (b : A) hole)))))
+(check-equal?
+ (term (reduce ,Δ= ,refl-elim))
+ (term zero))
diff --git a/cur-test/cur/tests/stdlib/bool.rkt b/cur-test/cur/tests/stdlib/bool.rkt
new file mode 100644
index 0000000..9de04bd
--- /dev/null
+++ b/cur-test/cur/tests/stdlib/bool.rkt
@@ -0,0 +1,18 @@
+#lang cur
+(require
+ rackunit
+ cur/stdlib/bool
+ cur/stdlib/sugar)
+
+(check-equal? (not true) false)
+(check-equal? (not false) true)
+
+(check-equal? (and true false) false)
+(check-equal? (and false false) true)
+(check-equal? (and false true) false)
+(check-equal? (and true true) true)
+
+(check-equal? (or true false) true)
+(check-equal? (or false false) false)
+(check-equal? (or false true) true)
+(check-equal? (or true true) true)
diff --git a/cur-test/cur/tests/stdlib/maybe.rkt b/cur-test/cur/tests/stdlib/maybe.rkt
new file mode 100644
index 0000000..4389a4c
--- /dev/null
+++ b/cur-test/cur/tests/stdlib/maybe.rkt
@@ -0,0 +1,21 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/maybe)
+
+(check-equal?
+ (some/i true)
+ (some Bool true))
+;; Disabled until #22 fixed
+#;(check-equal?
+   (case* Maybe Type (some Bool true) (Bool)
+          (lambda* (A : Type) (x : (Maybe A)) A)
+          [(none (A : Type)) IH: ()
+           false]
+          [(some (A : Type) (x : A)) IH: ()
+           ;; TODO: Don't know how to use dependency yet
+           (if x true false)])
+   true)
diff --git a/cur-test/cur/tests/stdlib/nat.rkt b/cur-test/cur/tests/stdlib/nat.rkt
new file mode 100644
index 0000000..d1de227
--- /dev/null
+++ b/cur-test/cur/tests/stdlib/nat.rkt
@@ -0,0 +1,32 @@
+#lang cur
+(require
+ cur/stdlib/sugar
+ cur/stdlib/nat
+ cur/stdlib/bool
+ rackunit)
+
+(check-equal? (add1 (s z)) (s (s z)))
+(check-equal? (sub1 (s z)) z)
+
+(check-equal? (plus z z) z)
+(check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z)))))
+
+(check-equal? (mult (s (s z)) z) z)
+(check-equal? (mult (s (s z)) (s z)) (s (s z)))
+
+;; TODO Disabled due to performance bugs
+#;(check-equal? (exp z z) (s z))
+#;(check-equal? (exp (s z) z) z)
+#;(check-equal? (square (s (s z))) (s (s (s (s z)))))
+
+(check-equal? (nat-equal? z z) true)
+(check-equal? (nat-equal? z (s z)) false)
+(check-equal? (nat-equal? (s z) (s z)) true)
+
+(check-equal? (even? z) true)
+(check-equal? (even? (s z)) false)
+(check-equal? (even? (s (s z))) true)
+(check-equal? (odd? z) false)
+(check-equal? (odd? (s z)) true)
+(check-equal? (odd? (s (s z))) false)
+(check-equal? (odd? (s (s (s z)))) true)
diff --git a/cur-test/cur/tests/stdlib/prop.rkt b/cur-test/cur/tests/stdlib/prop.rkt
new file mode 100644
index 0000000..a4a881a
--- /dev/null
+++ b/cur-test/cur/tests/stdlib/prop.rkt
@@ -0,0 +1,36 @@
+#lang cur
+(require
+ cur/stdlib/prop
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+ rackunit)
+
+(:: pf:anything-implies-true thm:anything-implies-true)
+(:: pf:and-is-symmetric thm:and-is-symmetric)
+(:: pf:proj1 thm:proj1)
+(:: pf:proj2 thm:proj2)
+(check-equal?
+ (elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
+       (λ* (A : Type) (x : A) z)
+       Bool
+       true
+       true
+       (refl Bool true))
+ z)
+
+(check-equal?
+ (conj/i (conj/i T T) T)
+ (conj (And True True) True (conj True True T T) T))
+
+(define (id (A : Type) (x : A)) x)
+
+(check-equal?
+ ((id (== True T T))
+  (refl True (run (id True T))))
+ (refl True T))
+
+(check-equal?
+ ((id (== True T T))
+  (refl True (id True T)))
+ (refl True T))
diff --git a/cur-test/cur/tests/stdlib/sartactics.rkt b/cur-test/cur/tests/stdlib/sartactics.rkt
new file mode 100644
index 0000000..88d70ef
--- /dev/null
+++ b/cur-test/cur/tests/stdlib/sartactics.rkt
@@ -0,0 +1,12 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/bool
+ cur/stdlib/sugar
+ cur/stdlib/tactics/base
+ cur/stdlib/tactics/sartactics)
+
+;; TODO: To much randomness for easy automated testing
+(define-theorem meow (forall (x : Bool) Bool))
+  #;(proof (interactive))
diff --git a/cur-test/cur/tests/stdlib/sugar.rkt b/cur-test/cur/tests/stdlib/sugar.rkt
new file mode 100644
index 0000000..d52b356
--- /dev/null
+++ b/cur-test/cur/tests/stdlib/sugar.rkt
@@ -0,0 +1,51 @@
+#lang cur
+(require
+ rackunit
+ cur/stdlib/sugar)
+
+;; TODO: Missing tests for match, others
+(check-equal?
+ ((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ ((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ ((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ (let ([x Type]
+       [y (λ (x : (Type 1)) x)])
+   (y x))
+ Type)
+
+(check-equal?
+ (let ([(x : (Type 1)) Type]
+       [y (λ (x : (Type 1)) x)])
+   (y x))
+ Type)
+
+;; check that raises decent syntax error
+;; Can't use this because (lambda () ...) and thunk are not things in Cur at runtime
+#;(check-exn
+   exn:fail:syntax?
+   (let ([x : (Type 1) Type]
+         [y (λ (x : (Type 1)) x)])
+     (y x)))
+
+;; check that raises type error
+#;(check-exn
+   exn:fail:syntax?
+   (let ([x uninferrable-expr]
+         [y (λ (x : (Type 1)) x)])
+     (y x)))
+
diff --git a/cur-test/cur/tests/stdlib/tactics.rkt b/cur-test/cur/tests/stdlib/tactics.rkt
new file mode 100644
index 0000000..c33d129
--- /dev/null
+++ b/cur-test/cur/tests/stdlib/tactics.rkt
@@ -0,0 +1,36 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/tactics/base
+ cur/stdlib/tactics/standard)
+(define-theorem meow (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+   (intro x)
+   (by-assumption)) true)
+ true)
+(define-theorem meow1 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+   (obvious)
+   ;; TODO: Add ability to check output
+   #;(print)) true)
+ true)
+(define-theorem meow2 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+  (intro x)
+  (restart)
+  (intro x)
+  (by-assumption)) true)
+ true)
+(define-theorem meow3 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof (obvious)) true)
+ true)
+;; TODO: Fix this unit test so it doesn't require interaction
+(define-theorem meow4 (forall (x : Bool) Bool))
+#;(proof (interactive))
diff --git a/cur-test/cur/tests/stdlib/typeclass.rkt b/cur-test/cur/tests/stdlib/typeclass.rkt
new file mode 100644
index 0000000..a0e9ab8
--- /dev/null
+++ b/cur-test/cur/tests/stdlib/typeclass.rkt
@@ -0,0 +1,30 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+ cur/stdlib/typeclass)
+
+(typeclass (Eqv (A : Type))
+           (equal? : (forall* (a : A) (b : A) Bool)))
+(impl (Eqv Bool)
+      (define (equal? (a : Bool) (b : Bool))
+        (if a
+            (if b true false)
+            (if b false true))))
+(impl (Eqv Nat)
+      (define equal? nat-equal?))
+(check-equal?
+ (equal? z z)
+ true)
+(check-equal?
+ (equal? z (s z))
+ false)
+(check-equal?
+ (equal? true false)
+ false)
+(check-equal?
+ (equal? true true)
+ true)
diff --git a/examples/stlc.rkt b/cur-test/cur/tests/stlc.rkt
similarity index 84%
rename from examples/stlc.rkt
rename to cur-test/cur/tests/stlc.rkt
index 4fa1e74..7143501 100644
--- a/examples/stlc.rkt
+++ b/cur-test/cur/tests/stlc.rkt
@@ -1,18 +1,19 @@
-#lang s-exp "../cur.rkt"
+#lang cur
 (require
-  "../stdlib/nat.rkt"
-  "../stdlib/sugar.rkt"
-  "../oll.rkt"
-  "../stdlib/maybe.rkt"
-  "../stdlib/bool.rkt"
-  "../stdlib/prop.rkt")
+ rackunit
+ cur/stdlib/nat
+ cur/stdlib/sugar
+ cur/oll
+ cur/stdlib/maybe
+ cur/stdlib/bool
+ cur/stdlib/prop)
 
 (define-language stlc
   #:vars (x)
   #:output-coq "stlc.v"
   #:output-latex "stlc.tex"
   (val  (v)   ::= true false unit)
-  ;; TODO: Allow datum as terminals
+  ;; TODO: Allow datum, like 1, as terminals
   (type (A B) ::= boolty unitty (-> A B) (* A A))
   (term (e)   ::= x v (app e e) (lambda (x : A) e) (cons e e)
                   (let (x x) = e in e)))
@@ -126,19 +127,17 @@
            #'stlc-unitty
            #'e)])))
 
-(module+ test
-  (require rackunit)
-  (check-equal?
-    (begin-stlc (lambda (x : 1) x))
-    (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
-  (check-equal?
-    (begin-stlc ((lambda (x : 1) x) ()))
-    (stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
-              (stlc-val-->-stlc-term stlc-unit)))
-  (check-equal?
-    (begin-stlc '(() ()))
-    (stlc-cons (stlc-val-->-stlc-term stlc-unit)
-               (stlc-val-->-stlc-term stlc-unit)))
-  (check-equal?
-    (begin-stlc #t)
-    (stlc-val-->-stlc-term stlc-true)))
+(check-equal?
+ (begin-stlc (lambda (x : 1) x))
+ (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
+(check-equal?
+ (begin-stlc ((lambda (x : 1) x) ()))
+ (stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
+           (stlc-val-->-stlc-term stlc-unit)))
+(check-equal?
+ (begin-stlc '(() ()))
+ (stlc-cons (stlc-val-->-stlc-term stlc-unit)
+            (stlc-val-->-stlc-term stlc-unit)))
+(check-equal?
+ (begin-stlc #t)
+ (stlc-val-->-stlc-term stlc-true))
diff --git a/cur-test/info.rkt b/cur-test/info.rkt
new file mode 100644
index 0000000..c042052
--- /dev/null
+++ b/cur-test/info.rkt
@@ -0,0 +1,7 @@
+#lang info
+(define collection 'multi)
+(define deps '())
+(define build-deps '("base" "rackunit-lib" ("cur-lib" #:version "0.2")))
+(define update-implies '("cur-lib"))
+(define pkg-desc "Tests for \"cur\".")
+(define pkg-authors '(wilbowma))
diff --git a/cur/info.rkt b/cur/info.rkt
new file mode 100644
index 0000000..b4cb13d
--- /dev/null
+++ b/cur/info.rkt
@@ -0,0 +1,6 @@
+#lang info
+(define collection 'multi)
+(define deps '("cur-lib" "cur-doc" "cur-test"))
+(define implies '("cur-lib" "cur-doc" "cur-test"))
+(define pkg-desc "Dependent types with parenthesis and meta-programming.")
+(define pkg-authors '(wilbowma))
diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt
deleted file mode 100644
index 61ec66b..0000000
--- a/curnel/redex-core.rkt
+++ /dev/null
@@ -1,1245 +0,0 @@
-#lang racket/base
-
-(require
-  racket/function
-  redex/reduction-semantics)
-
-(provide
-  (all-defined-out))
-
-(set-cache-size! 10000)
-
-;; Test suite setup.
-(module+ test
-  (require
-    rackunit
-    (only-in racket/set set=?))
-  (define-syntax-rule (check-holds (e ...))
-    (check-true
-      (judgment-holds (e ...))))
-  (define-syntax-rule (check-not-holds (e ...))
-    (check-false
-      (judgment-holds (e ...))))
-  (define-syntax-rule (check-equiv? e1 e2)
-    (check (default-equiv) e1 e2))
-  (define-syntax-rule (check-not-equiv? e1 e2)
-    (check (compose not (default-equiv)) e1 e2)))
-
-#| References:
- |  http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
- |  https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf
- |  http://www.emn.fr/z-info/ntabareau/papers/universe_polymorphism.pdf
- |  http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf
- |  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.74
- |  http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf
- |#
-
-#| ttL is the core language of Cur. Very similar to TT (Idirs core) and Luo's UTT. Surface
- | langauge should provide short-hand, such as -> for non-dependent function types, and type
- | inference.
- |#
-(define-language ttL
-  (i j k  ::= natural)
-  (U ::= (Unv i))
-  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e) (elim D U))
-  ;; Δ (signature). (inductive-name : type ((constructor : type) ...))
-  ;; NB: Δ is a map from a name x to a pair of it's type and a map of constructor names to their types
-  (Δ   ::= ∅ (Δ (D : t ((c : t) ...))))
-  (D x c ::= variable-not-otherwise-mentioned)
-  #:binding-forms
-  (λ (x : t) e #:refers-to x)
-  (Π (x : t_0) t_1 #:refers-to x))
-
-(define x? (redex-match? ttL x))
-(define t? (redex-match? ttL t))
-(define e? (redex-match? ttL e))
-(define U? (redex-match? ttL U))
-(define Δ? (redex-match? ttL Δ))
-
-(module+ test
-  (define-term Type (Unv 0))
-  (check-true (x? (term T)))
-  (check-true (x? (term A)))
-  (check-true (x? (term truth)))
-  (check-true (x? (term zero)))
-  (check-true (x? (term s)))
-  (check-true (t? (term zero)))
-  (check-true (t? (term s)))
-  (check-true (x? (term nat)))
-  (check-true (t? (term nat)))
-  (check-true (t? (term A)))
-  (check-true (t? (term S)))
-  (check-true (U? (term (Unv 0))))
-  (check-true (U? (term Type)))
-  (check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
-  (check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
-  (check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
-
-  ;; TODO: Rename these signatures, and use them in all future tests.
-  (define Δ (term ((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat)))))
-                        (bool : (Unv 0) ((true : bool) (false : bool))))))
-  (define Δ0 (term ∅))
-  (define Δ3 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ()))))
-  (define Δ4 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
-                             ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))))))
-  (check-true (Δ? Δ0))
-  (check-true (Δ? Δ))
-  (check-true (Δ? Δ4))
-  (check-true (Δ? Δ3))
-  (check-true (Δ? Δ4))
-  (define sigma (term ((((((∅ (true : (Unv 0) ((T : true))))
-                           (false : (Unv 0) ()))
-                          (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
-                                 ()))
-                         (nat : (Unv 0) ()))
-                        (heap : (Unv 0) ()))
-                       (pre : (Π (temp808 : heap) (Unv 0)) ()))))
-  (check-true (Δ? (term (∅ (true : (Unv 0) ((T : true)))))))
-  (check-true (Δ? (term (∅ (false : (Unv 0) ())))))
-  (check-true (Δ? (term (∅ (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
-                                  ())))))
-  (check-true (Δ? (term (∅ (nat : (Unv 0) ())))))
-  (check-true (Δ? (term (∅ (pre : (Π (temp808 : heap) (Unv 0)) ())))))
-
-  (check-true (Δ? (term ((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ())))))
-  (check-true (Δ? (term (((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ()))
-                                                            (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
-                                                                   ())))))
-  (check-true (Δ? sigma)))
-
-;;; ------------------------------------------------------------------------
-;;; Universe typing
-
-(define-judgment-form ttL
-  #:mode (unv-type I O)
-  #:contract (unv-type U U)
-
-  [(where i_1 ,(add1 (term i_0)))
-   -----------------
-   (unv-type (Unv i_0) (Unv i_1))])
-
-;; Universe predicativity rules. Impredicative in (Unv 0)
-(define-judgment-form ttL
-  #:mode (unv-pred I I O)
-  #:contract (unv-pred U U U)
-
-  [----------------
-   (unv-pred (Unv i) (Unv 0) (Unv 0))]
-
-  [(where i_3 ,(max (term i_1) (term i_2)))
-   ----------------
-   (unv-pred (Unv i_1) (Unv i_2) (Unv i_3))])
-
-(define-metafunction ttL
-  α-equivalent?  : t t -> #t or #f
-  [(α-equivalent? t_0 t_1)
-   ,(alpha-equivalent? ttL (term t_0) (term t_1))])
-
-(module+ test
-  (default-equiv (lambda (x y) (term (α-equivalent? ,x ,y)))))
-
-;; Replace x by t_1 in t_0
-(define-metafunction ttL
-  subst : t x t -> t
-  [(subst t_0 x t_1)
-   (substitute t_0 x t_1)])
-
-(module+ test
-  (check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
-  (check-true
-    (term
-      (α-equivalent?
-        (Π (a : S) (Π (b : B) ((and S) B)))
-        (subst (Π (a : A) (Π (b : B) ((and A) B))) A S)))))
-
-(define-metafunction ttL
-  subst-all : t (x ...) (e ...) -> t
-  [(subst-all t () ()) t]
-  [(subst-all t (x_0 x ...) (e_0 e ...))
-   (subst-all (subst t x_0 e_0) (x ...) (e ...))])
-
-;;; ------------------------------------------------------------------------
-;;; Primitive Operations on signatures Δ (those operations that do not require contexts)
-
-;;; TODO: Might be worth maintaining the above bijection between Δ and maps for performance reasons
-
-;; TODO: This is doing too many things
-;; NB: Depends on clause order
-(define-metafunction ttL
-  Δ-ref-type : Δ x -> t or #f
-  [(Δ-ref-type ∅ x) #f]
-  [(Δ-ref-type (Δ (x : t any)) x) t]
-  [(Δ-ref-type (Δ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t]
-  [(Δ-ref-type (Δ (x_0 : t_0 any)) x) (Δ-ref-type Δ x)])
-
-(define-metafunction ttL
-  Δ-set : Δ x t ((x : t) ...) -> Δ
-  [(Δ-set Δ x t any) (Δ (x : t any))])
-
-(define-metafunction ttL
-  Δ-union : Δ Δ -> Δ
-  [(Δ-union Δ ∅) Δ]
-  [(Δ-union Δ_2 (Δ_1 (x : t any)))
-   ((Δ-union Δ_2 Δ_1) (x : t any))])
-
-;; Returns the inductively defined type that x constructs
-;; NB: Depends on clause order
-(define-metafunction ttL
-  Δ-key-by-constructor : Δ x -> x
-  [(Δ-key-by-constructor (Δ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c)
-   x]
-  [(Δ-key-by-constructor (Δ (x_1 : t_1 any)) x)
-   (Δ-key-by-constructor Δ x)])
-
-(module+ test
-  (check-equal?
-    (term (Δ-key-by-constructor ,Δ zero))
-    (term nat))
-  (check-equal?
-    (term (Δ-key-by-constructor ,Δ s))
-    (term nat)))
-
-;; Returns the constructor map for the inductively defined type x_D in the signature Δ
-(define-metafunction ttL
-  Δ-ref-constructor-map : Δ x -> ((x : t) ...) or #f
-  ;; NB: Depends on clause order
-  [(Δ-ref-constructor-map ∅ x_D) #f]
-  [(Δ-ref-constructor-map (Δ (x_D : t_D any)) x_D)
-   any]
-  [(Δ-ref-constructor-map (Δ (x_1 : t_1 any)) x_D)
-   (Δ-ref-constructor-map Δ x_D)])
-
-(module+ test
-  (check-equal?
-    (term (Δ-ref-constructor-map ,Δ nat))
-    (term ((zero : nat) (s : (Π (x : nat) nat)))))
-  (check-equal?
-    (term (Δ-ref-constructor-map ,sigma false))
-    (term ())))
-
-;; TODO: Should not use Δ-ref-type
-(define-metafunction ttL
-  Δ-ref-constructor-type : Δ x x -> t
-  [(Δ-ref-constructor-type Δ x_D x_ci)
-   (Δ-ref-type Δ x_ci)])
-
-;; Get the list of constructors for the inducitvely defined type x_D
-;; NB: Depends on clause order
-(define-metafunction ttL
-  Δ-ref-constructors : Δ x -> (x ...) or #f
-  [(Δ-ref-constructors ∅ x_D) #f]
-  [(Δ-ref-constructors (Δ (x_D : t_D ((x : t) ...))) x_D)
-   (x ...)]
-  [(Δ-ref-constructors (Δ (x_1 : t_1 any)) x_D)
-   (Δ-ref-constructors Δ x_D)])
-
-;; NB: Depends on clause order
-(define-metafunction ttL
-  sequence-index-of : any (any ...) -> natural
-  [(sequence-index-of any_0 (any_0 any ...))
-   0]
-  [(sequence-index-of any_0 (any_1 any ...))
-   ,(add1 (term (sequence-index-of any_0 (any ...))))])
-
-;; Get the index of the constructor x_ci in the list of constructors for x_D
-(define-metafunction ttL
-  Δ-constructor-index : Δ x x -> natural
-  [(Δ-constructor-index Δ x_D x_ci)
-   (sequence-index-of x_ci (Δ-ref-constructors Δ x_D))])
-
-;;; ------------------------------------------------------------------------
-;;; Operations that involve contexts.
-
-(define-extended-language tt-ctxtL ttL
-  ;; Telescope.
-  ;; NB: There is a bijection between this an a vector of maps from x to t
-  (Ξ Φ ::= hole (Π (x : t) Ξ))
-  ;; Apply context
-  ;; NB: There is a bijection between this an a vector expressions
-  (Θ   ::= hole (Θ e)))
-
-(define Ξ? (redex-match? tt-ctxtL Ξ))
-(define Φ? (redex-match? tt-ctxtL Φ))
-(define Θ? (redex-match? tt-ctxtL Θ))
-
-(module+ test
-  ;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed
-  (define (telescope-equiv x y)
-    (alpha-equivalent? ttL (term (in-hole ,x (Unv 0))) (term (in-hole ,y (Unv 0)))))
-  (define-syntax-rule (check-telescope-equiv? e1 e2)
-    (check telescope-equiv e1 e2))
-  (define-syntax-rule (check-telescope-not-equiv? e1 e2)
-    (check (compose not telescope-equiv) e1 e2)))
-
-;; TODO: Might be worth it to actually maintain the above bijections, for performance reasons.
-
-;; Return the parameters of x_D as a telescope Ξ
-;; TODO: Define generic traversals of Δ and Γ ?
-(define-metafunction tt-ctxtL
-  Δ-ref-parameter-Ξ : Δ x -> Ξ
-  [(Δ-ref-parameter-Ξ (Δ (x_D : (in-hole Ξ U) any)) x_D)
-   Ξ]
-  [(Δ-ref-parameter-Ξ (Δ (x_1 : t_1 any)) x_D)
-   (Δ-ref-parameter-Ξ Δ x_D)])
-
-(module+ test
-  (check-telescope-equiv?
-    (term (Δ-ref-parameter-Ξ ,Δ nat))
-    (term hole))
-  (check-telescope-equiv?
-    (term (Δ-ref-parameter-Ξ ,Δ4 and))
-    (term (Π (A : Type) (Π (B : Type) hole)))))
-
-;; Applies the term t to the telescope Ξ.
-;; TODO: Test
-#| TODO:
- | This essentially eta-expands t at the type-level. Why is this necessary? Shouldn't it be true
- | that (equivalent t (Ξ-apply Ξ t))?
- | Maybe not. t is a lambda whose type is equivalent to (Ξ-apply Ξ t)? Yes.
- |#
-(define-metafunction tt-ctxtL
-  Ξ-apply : Ξ t -> t
-  [(Ξ-apply hole t) t]
-  [(Ξ-apply (Π (x : t) Ξ) t_0) (Ξ-apply Ξ (t_0 x))])
-
-;; Compose multiple telescopes into a single telescope:
-(define-metafunction tt-ctxtL
-  Ξ-compose : Ξ Ξ ... -> Ξ
-  [(Ξ-compose Ξ) Ξ]
-  [(Ξ-compose Ξ_0 Ξ_1 Ξ_rest ...)
-   (Ξ-compose (in-hole Ξ_0 Ξ_1) Ξ_rest ...)])
-
-(module+ test
-  (check-telescope-equiv?
-    (term (Ξ-compose
-            (Π (x : t_0) (Π (y : t_1) hole))
-            (Π (z : t_2) (Π (a : t_3) hole))))
-    (term (Π (x : t_0) (Π (y : t_1) (Π (z : t_2) (Π (a : t_3) hole)))))))
-
-;; Compute the number of arguments in a Ξ
-(define-metafunction tt-ctxtL
-  Ξ-length : Ξ -> natural
-  [(Ξ-length hole) 0]
-  [(Ξ-length (Π (x : t) Ξ)) ,(add1 (term (Ξ-length Ξ)))])
-
-;; Compute the number of applications in a Θ
-(define-metafunction tt-ctxtL
-  Θ-length : Θ -> natural
-  [(Θ-length hole) 0]
-  [(Θ-length (Θ e)) ,(add1 (term (Θ-length Θ)))])
-
-;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole.
-(define-metafunction tt-ctxtL
-  Θ-ref : Θ natural -> e or #f
-  [(Θ-ref hole natural) #f]
-  [(Θ-ref (in-hole Θ (hole e)) 0) e]
-  [(Θ-ref (in-hole Θ (hole e)) natural) (Θ-ref Θ ,(sub1 (term natural)))])
-
-;;; ------------------------------------------------------------------------
-;;; Computing the types of eliminators
-
-;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D
-(define-metafunction tt-ctxtL
-  Δ-constructor-telescope : Δ x x -> Ξ
-  [(Δ-constructor-telescope Δ x_D x_ci)
-   Ξ
-   (where (in-hole Ξ (in-hole Θ x_D))
-     (Δ-ref-constructor-type Δ x_D x_ci))])
-
-;; Returns the parameter arguments as an apply context of the constructor x_ci of the inductively
-;; defined type x_D
-(define-metafunction tt-ctxtL
-  Δ-constructor-parameters : Δ x x -> Θ
-  [(Δ-constructor-parameters Δ x_D x_ci)
-   Θ
-   (where (in-hole Ξ (in-hole Θ x_D))
-     (Δ-ref-constructor-type Δ x_D x_ci))])
-
-;; Inner loop for Δ-constructor-noninductive-telescope
-(define-metafunction tt-ctxtL
-  noninductive-loop : x Φ -> Φ
-  [(noninductive-loop x_D hole) hole]
-  [(noninductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
-   (noninductive-loop x_D Φ_1)]
-  [(noninductive-loop x_D (Π (x : t) Φ_1))
-   (Π (x : t) (noninductive-loop x_D Φ_1))])
-
-;; Returns the noninductive arguments to the constructor x_ci of the inductively defined type x_D
-(define-metafunction tt-ctxtL
-  Δ-constructor-noninductive-telescope : Δ x x -> Ξ
-  [(Δ-constructor-noninductive-telescope Δ x_D x_ci)
-   (noninductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
-
-;; Inner loop for Δ-constructor-inductive-telescope
-;; NB: Depends on clause order
-(define-metafunction tt-ctxtL
-  inductive-loop : x Φ -> Φ
-  [(inductive-loop x_D hole) hole]
-  [(inductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
-   (Π (x : (in-hole Φ (in-hole Θ x_D))) (inductive-loop x_D Φ_1))]
-  [(inductive-loop x_D (Π (x : t) Φ_1))
-   (inductive-loop x_D Φ_1)])
-
-;; Returns the inductive arguments to the constructor x_ci of the inducitvely defined type x_D
-(define-metafunction tt-ctxtL
-  Δ-constructor-inductive-telescope : Δ x x -> Ξ
-  [(Δ-constructor-inductive-telescope Δ x_D x_ci)
-   (inductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
-
-;; Returns the inductive hypotheses required for eliminating the inductively defined type x_D with
-;; motive t_P, where the telescope Φ are the inductive arguments to a constructor for x_D
-(define-metafunction tt-ctxtL
-  hypotheses-loop : x t Φ -> Φ
-  [(hypotheses-loop x_D t_P hole) hole]
-  [(hypotheses-loop x_D t_P (name any_0 (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1)))
-   ;; TODO: Instead of this nonsense, it might be simpler to pass in the type of t_P and use that
-   ;; as/to compute the type of the hypothesis.
-   (Π (x_h : (in-hole Φ ((in-hole Θ t_P) (Ξ-apply Φ x))))
-      (hypotheses-loop x_D t_P Φ_1))
-   (where x_h ,(variable-not-in (term (x_D t_P any_0)) 'x-ih))])
-
-;; Returns the inductive hypotheses required for the elimination method of constructor x_ci for
-;; inductive type x_D, when eliminating with motive t_P.
-(define-metafunction tt-ctxtL
-  Δ-constructor-inductive-hypotheses : Δ x x t -> Ξ
-  [(Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P)
-   (hypotheses-loop x_D t_P (Δ-constructor-inductive-telescope Δ x_D x_ci))])
-
-(define-metafunction tt-ctxtL
-  Δ-constructor-method-telescope : Δ x x t -> Ξ
-  [(Δ-constructor-method-telescope Δ x_D x_ci t_P)
-   (Π (x_mi : (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a x_ci)))))
-      hole)
-   (where Θ_p (Δ-constructor-parameters Δ x_D x_ci))
-   (where Ξ_a (Δ-constructor-telescope Δ x_D x_ci))
-   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P))
-   (where x_mi ,(variable-not-in (term (t_P Δ)) 'x-mi))])
-
-;; fold Ξ-compose over map Δ-constructor-method-telescope over the list of constructors
-(define-metafunction tt-ctxtL
-  method-loop : Δ x t (x ...) -> Ξ
-  [(method-loop Δ x_D t_P ()) hole]
-  [(method-loop Δ x_D t_P (x_0 x_rest ...))
-   (Ξ-compose (Δ-constructor-method-telescope Δ x_D x_0 t_P) (method-loop Δ x_D t_P (x_rest ...)))])
-
-;; Returns the telescope of all methods required to eliminate the type x_D with motive t_P
-(define-metafunction tt-ctxtL
-  Δ-methods-telescope : Δ x t -> Ξ
-  [(Δ-methods-telescope Δ x_D t_P)
-   (method-loop Δ x_D t_P (Δ-ref-constructors Δ x_D))])
-
-(module+ test
-  (check-telescope-equiv?
-    (term (Δ-methods-telescope ,Δ nat (λ (x : nat) nat)))
-    (term (Π (m-zero : ((λ (x : nat) nat) zero))
-             (Π (m-s : (Π (x : nat) (Π (x-ih : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x))))) hole))))
-  (check-telescope-equiv?
-    (term (Δ-methods-telescope ,Δ nat P))
-    (term (Π (m-zero : (P zero))
-             (Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x)))))
-                hole))))
-  (check-telescope-equiv?
-    (term (Δ-methods-telescope ,Δ  nat (λ (x : nat) nat)))
-    (term (Π (m-zero :  ((λ (x : nat) nat) zero))
-             (Π (m-s : (Π (x : nat) (Π (ih-x : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x)))))
-                hole))))
-  (check-telescope-equiv?
-    (term (Δ-methods-telescope ,Δ4 and (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))))
-    (term (Π (m-conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B)
-                                                                      ((((λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
-                                                                         A)
-                                                                        B)
-                                                                       ((((conj A) B) a) b)))))))
-             hole)))
-  (check-true (x? (term false)))
-  (check-true (Ξ? (term hole)))
-  (check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
-  (check-true (redex-match? ttL ((x : t) ...) (term ())))
-  (check-telescope-equiv?
-    (term (Δ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x))))
-    (term hole)))
-
-;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
-;; is in universe U.
-;;
-;; The type of (elim x_D U) is something like:
-;;  (∀ (P : (∀ a -> ... -> (D a ...) -> U))
-;;     (method_ci ...) -> ... ->
-;;     (a -> ... -> (D a ...) ->
-;;       (P a ... (D a ...))))
-;;
-;; x_D   is an inductively defined type
-;; U     is the sort the motive
-;; x_P   is the name of the motive
-;; Ξ_P*D is the telescope of the parameters of x_D and
-;;       the witness of type x_D (applied to the parameters)
-;; Ξ_m   is the telescope of the methods for x_D
-(define-metafunction tt-ctxtL
-  Δ-elim-type : Δ x U -> t
-  [(Δ-elim-type Δ x_D U)
-   (Π (x_P : (in-hole Ξ_P*D U))
-      ;; The methods Ξ_m for each constructor of type x_D
-      (in-hole Ξ_m
-        ;; And finally, the parameters and discriminant
-        (in-hole Ξ_P*D
-          ;; The result is (P a ... (x_D a ...)), i.e., the motive
-          ;; applied to the paramters and discriminant
-          (Ξ-apply Ξ_P*D x_P))))
-   ;; Get the parameters of x_D
-   (where Ξ (Δ-ref-parameter-Ξ Δ x_D))
-   ;; A fresh name to bind the discriminant
-   (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
-   ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
-   ;; of the parameters and the inductive type applied to the
-   ;; parameters
-   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole)))
-   ;; A fresh name for the motive
-   (where x_P ,(variable-not-in (term (Δ Γ x_D Ξ Ξ_P*D x)) 'x-P))
-   ;; The types of the methods for this inductive.
-   (where Ξ_m (Δ-methods-telescope Δ x_D x_P))])
-
-;; TODO: This might belong in the next section, since it's related to evaluation
-;; Generate recursive applications of the eliminator for each inductive argument of type x_D.
-;; In more detaill, given motive t_P, parameters Θ_p, methods Θ_m, and arguments Θ_i to constructor
-;; x_ci for x_D, for each inductively smaller term t_i of type (in-hole Θ_p x_D) inside Θ_i,
-;; generate: (elim x_D U t_P  Θ_m ... Θ_p ... t_i)
-(define-metafunction tt-ctxtL
-  Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (in-hole Θ_i (hole (name t_i (in-hole Θ_r x_ci)))))
-   ((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
-    (in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
-   (side-condition (memq (term x_ci) (term (Δ-ref-constructors Δ x_D))))]
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_nr) hole])
-
-;; TODO: Insufficient tests, no tests of inductives with parameters, or complex induction.
-(module+ test
-  (check-true
-    (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
-  (check-telescope-equiv?
-    (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
-                      ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                      (hole zero)))
-    (term (hole (((((elim nat Type) (λ (x : nat) nat))
-                   (s zero))
-                  (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                 zero))))
-  (check-telescope-equiv?
-    (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
-                      ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                      (hole (s zero))))
-    (term (hole (((((elim nat Type) (λ (x : nat) nat))
-                   (s zero))
-                  (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                 (s zero))))))
-
-;;; ------------------------------------------------------------------------
-;;; Dynamic semantics
-;;; The majority of this section is dedicated to evaluation of (elim x U), the eliminator for the
-;;; inductively defined type x with a motive whose result is in universe U
-
-(define-extended-language tt-redL tt-ctxtL
-  ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. However,
-  ;; determining whether or not it is partially applied cannot be done with the grammar alone.
-  (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U)))
-  (Θv  ::= hole (Θv v))
-  ;; call-by-value, plus reduce under Π (helps with typing checking)
-  (E   ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)))
-
-(define Θv? (redex-match? tt-redL Θv))
-(define E? (redex-match? tt-redL E))
-(define v? (redex-match? tt-redL v))
-
-(module+ test
-  (check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
-  (check-true (v? (term (refl Nat))))
-  (check-true (v? (term ((refl Nat) z)))))
-
-(define tt-->
-  (reduction-relation tt-redL
-    (--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2)))
-         (Δ (in-hole E (subst t_1 x t_2)))
-         -->β)
-    (--> (Δ (in-hole E (in-hole Θv ((elim x_D U) v_P))))
-         (Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
-         #|
-          | The elim form must appear applied like so:
-          | (elim x_D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
-          |
-          | Where:
-          |   x_D       is the inductive being eliminated
-          |   U         is the universe of the result of the motive
-          |   v_P       is the motive
-          |   m_{0..n}  are the methods
-          |   p ...     are the parameters of x_D
-          |   c_i       is a constructor of x_d
-          |   a ...     are the arguments to c_i
-          | Unfortunately, Θ contexts turn all this inside out:
-          | TODO: Write better abstractions for this notation
-          |#
-          ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
-          ;; the discriminant: the constructor x_ci applied to its argument Θv_i
-         (where (in-hole (Θv_p (in-hole Θv_i x_ci)) Θv_m) Θv)
-         ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
-         ;; arguments.
-         (side-condition (equal? (term (Θ-length Θv_p)) (term (Ξ-length (Δ-ref-parameter-Ξ Δ x_D)))))
-         ;; Ensure x_ci is actually a constructor for x_D
-         (where (x_c* ...) (Δ-ref-constructors Δ x_D))
-         (side-condition (memq (term x_ci) (term (x_c* ...))))
-         ;; There should be a number of methods equal to the number of constructors; to ensure E
-         ;; doesn't capture methods and Θv_m doesn't capture other arguments
-         (side-condition (equal? (length (term (x_c* ...)))  (term (Θ-length Θv_m))))
-         ;; Find the method for constructor x_ci, relying on the order of the arguments.
-         (where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ x_D x_ci)))
-         ;; Generate the inductive recursion
-         (where Θ_r (Δ-inductive-elim Δ x_D U v_P Θv_p Θv_m Θv_i))
-         -->elim)))
-
-(define-metafunction tt-redL
-  step : Δ e -> e
-  [(step Δ e)
-   e_r
-   (where (_ e_r) ,(car (apply-reduction-relation tt--> (term (Δ e)))))])
-
-(define-metafunction tt-redL
-  reduce : Δ e -> e
-  [(reduce Δ e)
-   e_r
-   (where (_ e_r)
-     ,(let ([r (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)])
-        ;; Efficient check for (= (length r) 1)
-        ;; NB: Check is overly aggressive and produces wrong error,
-        ;; because not reducing under lambda.
-        #;(unless (null? (cdr r))
-          (error "Church-Rosser broken" r))
-        (car r)))])
-
-;; TODO: Move equivalence up here, and use in these tests.
-(module+ test
-  (check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
-  (check-equiv? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
-  (check-not-equiv? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
-  (check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
-                (term (Π (x : t) (Unv 0))))
-  (check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
-                  (term (Π (x : t) (x x))))
-  (check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
-                                                       (s zero))
-                                    (λ (x : nat) (λ (ih-x : nat)
-                                                        (s (s x)))))
-                                   zero)))
-                (term (s zero)))
-  (check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
-                                                       (s zero))
-                                    (λ (x : nat) (λ (ih-x : nat)
-                                                        (s (s x)))))
-                                   (s zero))))
-                (term (s (s zero))))
-  (check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
-                                                       (s zero))
-                                    (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                                   (s (s (s zero))))))
-                (term (s (s (s (s zero))))))
-
-  (check-equiv?
-    (term (reduce ,Δ
-                  (((((elim nat Type) (λ (x : nat) nat))
-                     (s (s zero)))
-                    (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-                   (s (s zero)))))
-    (term (s (s (s (s zero))))))
-  (check-equiv?
-    (term (step ,Δ
-                  (((((elim nat Type) (λ (x : nat) nat))
-                     (s (s zero)))
-                    (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-                   (s (s zero)))))
-    (term
-      (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
-        (s zero))
-       (((((elim nat Type) (λ (x : nat) nat))
-          (s (s zero)))
-         (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-        (s zero)))))
-  (check-equiv?
-    (term (step ,Δ (step ,Δ
-                 (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
-                   (s zero))
-                  (((((elim nat Type) (λ (x : nat) nat))
-                     (s (s zero)))
-                    (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-                   (s zero))))))
-    (term
-      ((λ (ih-x1 : nat) (s ih-x1))
-       (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
-         zero)
-        (((((elim nat Type) (λ (x : nat) nat))
-           (s (s zero)))
-          (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-         zero))))))
-
-(define-judgment-form tt-redL
-  #:mode (equivalent I I I)
-  #:contract (equivalent Δ t t)
-
-  [(where t_2 (reduce Δ t_0))
-   (where t_3 (reduce Δ t_1))
-   (side-condition (α-equivalent? t_2 t_3))
-   ----------------- "≡-αβ"
-   (equivalent Δ t_0 t_1)])
-(module+ test
-  (define-syntax-rule (check-equivalent e1 e2)
-    (check-holds (equivalent ∅ e1 e2)))
-  (check-equivalent
-    (λ (x : Type) x) (λ (y : Type) y))
-  (check-equivalent
-    (Π (x : Type) x) (Π (y : Type) y)))
-
-;;; ------------------------------------------------------------------------
-;;; Type checking and synthesis
-
-(define-extended-language tt-typingL tt-redL
-  ;; NB: There may be a bijection between Γ and Ξ. That's interesting.
-  ;; NB: Also a bijection between Γ and a list of maps from x to t.
-  (Γ   ::= ∅ (Γ x : t)))
-(define Γ? (redex-match? tt-typingL Γ))
-
-(define-metafunction tt-typingL
-  Γ-union : Γ Γ -> Γ
-  [(Γ-union Γ ∅) Γ]
-  [(Γ-union Γ_2 (Γ_1 x : t))
-   ((Γ-union Γ_2 Γ_1) x : t)])
-
-(define-metafunction tt-typingL
-  Γ-set : Γ x t -> Γ
-  [(Γ-set Γ x t) (Γ x : t)])
-
-;; NB: Depends on clause order
-(define-metafunction tt-typingL
-  Γ-ref : Γ x -> t or #f
-  [(Γ-ref ∅ x) #f]
-  [(Γ-ref (Γ x : t) x) t]
-  [(Γ-ref (Γ x_0 : t_0) x_1) (Γ-ref Γ x_1)])
-
-;; NB: Depends on clause order
-(define-metafunction tt-typingL
-  Γ-remove : Γ x -> Γ
-  [(Γ-remove ∅ x) ∅]
-  [(Γ-remove (Γ x : t) x) Γ]
-  [(Γ-remove (Γ x_0 : t_0) x_1) (Γ-remove Γ x_1)])
-
-(define-metafunction tt-typingL
-  nonpositive : x t -> #t or #f
-  [(nonpositive x (in-hole Θ x))
-   #t]
-  [(nonpositive x (Π (x_0 : (in-hole Θ x)) t))
-   #f]
-  [(nonpositive x (Π (x_0 : t_0) t))
-   ,(and (term (positive x t_0)) (term (nonpositive x t)))]
-  [(nonpositive x t) #t])
-
-(define-metafunction tt-typingL
-  positive : x t -> #t or #f
-  [(positive x (in-hole Θ x))
-   #f]
-  [(positive x (Π (x_0 : (in-hole Θ x)) t))
-   (positive x t)]
-  [(positive x (Π (x_0 : t_0) t))
-   ,(and (term (nonpositive x t_0)) (term (positive x t)))]
-  [(positive x t) #t])
-
-(define-metafunction tt-typingL
-  positive* : x (t ...) -> #t or #f
-  [(positive* x_D ()) #t]
-  [(positive* x_D (t_c t_rest ...))
-   ;; Replace the result of the constructor with (Unv 0), to avoid the result being considered a
-   ;; nonpositive position.
-   ,(and (term (positive x_D (in-hole Ξ (Unv 0)))) (term (positive* x_D (t_rest ...))))
-   (where (in-hole Ξ (in-hole Θ x_D)) t_c)])
-
-;; NB: These tests may or may not fail because positivity checking is not implemented.
-(module+ test
-  (check-true (term (positive* nat (nat))))
-  (check-true (term (positive* nat ((Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))))
-  (check-true (term (positive* nat ((Π (x : nat) nat)))))
-  ;; (nat -> nat) -> nat
-  ;; Not sure if this is actually supposed to pass
-  (check-false (term (positive* nat ((Π (x : (Π (y : nat) nat)) nat)))))
-  ;; ((Unv 0) -> nat) -> nat
-  (check-true (term (positive* nat ((Π (x : (Π (y : (Unv 0)) nat)) nat)))))
-  ;; (((nat -> (Unv 0)) -> nat) -> nat)
-  (check-true (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))))
-  ;; Not sure if this is actually supposed to pass
-  ;; ((nat -> nat) -> nat) -> nat
-  (check-false (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat))))))
-
-;; Holds when the signature Δ and typing context Γ are well-formed.
-(define-judgment-form tt-typingL
-  #:mode (wf I I)
-  #:contract (wf Δ Γ)
-
-  [----------------- "WF-Empty"
-   (wf ∅ ∅)]
-
-  [(type-infer Δ Γ t t_0)
-   (wf Δ Γ)
-   ----------------- "WF-Var"
-   (wf Δ (Γ x : t))]
-
-  [(wf Δ ∅)
-   (type-infer Δ ∅ t_D U_D)
-   (type-infer Δ (∅ x_D : t_D) t_c U_c) ...
-   ;; NB: Ugh this should be possible with pattern matching alone ....
-   (side-condition ,(map (curry equal? (term x_D)) (term (x_D* ...))))
-   (side-condition (positive* x_D (t_c ...)))
-   ----------------- "WF-Inductive"
-   (wf (Δ (x_D : t_D
-               ;; Checks that a constructor for x actually produces an x, i.e., that
-               ;; the constructor is well-formed.
-               ((x_c : (name t_c (in-hole Ξ (in-hole Θ x_D*)))) ...))) ∅)])
-
-(module+ test
-  (check-true (judgment-holds (wf ,Δ0 ∅)))
-  (check-true (redex-match? tt-redL (in-hole Ξ (Unv 0)) (term (Unv 0))))
-  (check-true (redex-match? tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
-                            (term (Π (x : nat) nat))))
-  (define (bindings-equal? l1 l2)
-    (map set=? l1 l2))
-  (check-pred
-    (curry bindings-equal?
-           (list (list
-                   (make-bind 'Ξ (term (Π (x : nat) hole)))
-                   (make-bind 'Φ (term hole))
-                   (make-bind 'Θ (term hole)))
-                 (list
-                   (make-bind 'Ξ (term hole))
-                   (make-bind 'Φ (term (Π (x : nat) hole)))
-                   (make-bind 'Θ (term hole)))))
-    (map match-bindings (redex-match tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
-                                     (term (Π (x : nat) nat)))))
-  (check-pred
-    (curry bindings-equal?
-           (list
-             (list
-               (make-bind 'Φ (term (Π (x : nat) hole)))
-               (make-bind 'Θ (term hole)))))
-    (map match-bindings (redex-match tt-redL (in-hole hole (in-hole Φ (in-hole Θ nat)))
-                                     (term (Π (x : nat) nat)))))
-
-  (check-true
-    (redex-match? tt-redL
-                  (in-hole hole (in-hole hole (in-hole hole nat)))
-                  (term nat)))
-  (check-true
-    (redex-match? tt-redL
-                  (in-hole hole (in-hole (Π (x : nat) hole) (in-hole hole nat)))
-                  (term (Π (x : nat) nat))))
-  (check-holds (wf (∅ (nat : (Unv 0) ())) ∅))
-
-  (check-holds (wf ,Δ0 ∅))
-  (check-holds (type-infer ∅ ∅ (Unv 0) U))
-  (check-holds (type-infer ∅ (∅ nat : (Unv 0)) nat U))
-  (check-holds (type-infer ∅ (∅ nat : (Unv 0)) (Π (x : nat) nat) U))
-  (check-true (term (positive* nat (nat (Π (x : nat) nat)))))
-  (check-holds
-    (wf (∅ (nat : (Unv 0) ((zero : nat)))) ∅))
-  (check-holds
-    (wf (∅ (nat : (Unv 0) ((s : (Π (x : nat) nat))))) ∅))
-  (check-holds (wf ,Δ ∅))
-
-  (check-holds (wf ,Δ3 ∅))
-  (check-holds (wf ,Δ4 ∅))
-  (check-holds (wf (∅ (truth : (Unv 0) ())) ∅))
-  (check-holds (wf ∅ (∅ x : (Unv 0))))
-  (check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : nat)))
-  (check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : (Π (x : nat) nat)))))
-
-
-;; TODO: Bi-directional and inference?
-;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
-
-;; Holds when e has type t under signature Δ and typing context Γ
-(define-judgment-form tt-typingL
-  #:mode (type-infer I I I O)
-  #:contract (type-infer Δ Γ e t)
-
-  [(wf Δ Γ)
-   (unv-type U_0 U_1)
-   ----------------- "DTR-Unv"
-   (type-infer Δ Γ U_0 U_1)]
-
-  [(where t (Δ-ref-type Δ x))
-   ----------------- "DTR-Inductive"
-   (type-infer Δ Γ x t)]
-
-  [(where t (Γ-ref Γ x))
-   ----------------- "DTR-Start"
-   (type-infer Δ Γ x t)]
-
-  [(type-infer Δ (Γ x : t_0) e t_1)
-   (type-infer Δ Γ (Π (x : t_0) t_1) U)
-   ----------------- "DTR-Abstraction"
-   (type-infer Δ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
-
-  [(type-infer Δ Γ t_0 U_1)
-   (type-infer Δ (Γ x : t_0) t U_2)
-   (unv-pred U_1 U_2 U)
-   ----------------- "DTR-Product"
-   (type-infer Δ Γ (Π (x : t_0) t) U)]
-
-  [(type-infer Δ Γ e_0 t)
-   ;; Cannot rely on type-infer producing normal forms.
-   (where (Π (x_0 : t_0) t_1) (reduce Δ t))
-   (type-check Δ Γ e_1 t_0)
-   (where t_3 (subst t_1 x_0 e_1))
-   ----------------- "DTR-Application"
-   (type-infer Δ Γ (e_0 e_1) t_3)]
-
-  [(where t (Δ-elim-type Δ D U))
-   (type-infer Δ Γ t U_e)
-   ----------------- "DTR-Elim_D"
-   (type-infer Δ Γ (elim D U) t)])
-
-(define-judgment-form tt-typingL
-  #:mode (type-check I I I I)
-  #:contract (type-check Δ Γ e t)
-
-  [(type-infer Δ Γ e t_0)
-   (equivalent Δ t t_0)
-   ----------------- "DTR-Check"
-   (type-check Δ Γ e t)])
-
-(module+ test
-  (check-holds (type-infer ∅ ∅ (Unv 0) (Unv 1)))
-  (check-holds (type-infer ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1)))
-  (check-holds (type-infer ∅ (∅ x : (Unv 0)) x (Unv 0)))
-  (check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
-                           (Π (x_3 : x_0) x_1) (Unv 0)))
-  (check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) x_0 U_1))
-  (check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2))
-  (check-holds (unv-pred (Unv 0) (Unv 0) (Unv 0)))
-  (check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t))
-
-  (check-holds (type-check ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))
-  (check-holds (type-check ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
-                           (Π (y : (Unv 0)) (Π (x : y) y))))
-
-  (check-equal? (list (term (Unv 1)))
-                (judgment-holds
-                  (type-infer ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))
-                              U)
-                  U))
-  ;; ---- Elim
-  ;; TODO: Clean up/Reorganize these tests
-  (check-true
-    (redex-match? tt-typingL
-                    (in-hole Θ_m (((elim x_D U) e_D) e_P))
-                    (term ((((elim truth Type) T) (Π (x : truth) (Unv 1))) (Unv 0)))))
-  (define Δtruth (term (∅ (truth : (Unv 0) ((T : truth))))))
-  (check-holds (type-infer ,Δtruth ∅ truth (in-hole Ξ U)))
-  (check-holds (type-infer ,Δtruth ∅ T (in-hole Θ_ai truth)))
-  (check-holds (type-infer ,Δtruth ∅ (λ (x : truth) (Unv 1))
-                           (in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
-
-  (check-telescope-equiv?
-    (term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
-    (term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole)))
-  (check-holds (type-infer ,Δtruth ∅ (elim truth Type) t))
-  (check-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
-                           ∅
-                           ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
-                            T)
-                           (Unv 1)))
-  (check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
-                               ∅
-                               ((((elim truth (Unv 1)) Type) Type) T)
-                               (Unv 1)))
-  (check-holds
-    (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
-  (check-holds
-    (type-infer ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))))
-                t))
-  (check-holds
-    (type-infer ,Δ ∅ nat (in-hole Ξ U)))
-  (check-holds
-    (type-infer ,Δ ∅ zero (in-hole Θ_ai nat)))
-  (check-holds
-    (type-infer ,Δ ∅ (λ (x : nat) nat)
-                (in-hole Ξ (Π (x : (in-hole Θ nat)) U))))
-  (define-syntax-rule (nat-test syn ...)
-    (check-holds (type-check ,Δ syn ...)))
-  (nat-test ∅ (Π (x : nat) nat) (Unv 0))
-  (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
-  (nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero)
-                                    (λ (x : nat) (λ (ih-x : nat) x))) zero)
-            nat)
-  (nat-test ∅ nat (Unv 0))
-  (nat-test ∅ zero nat)
-  (nat-test ∅ s (Π (x : nat) nat))
-  (nat-test ∅ (s zero) nat)
-  ;; TODO: Meta-function auto-currying and such
-  (check-holds
-      (type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat))
-                           zero)
-                           (λ (x : nat) (λ (ih-x : nat) x)))
-                  t))
-  (nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
-                    zero)
-                    (λ (x : nat) (λ (ih-x : nat) x)))
-                   zero)
-              nat)
-  (nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
-                    (s zero))
-                    (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                   zero)
-              nat)
-  (nat-test ∅ (((((elim nat Type) (λ (x : nat) nat))
-                              (s zero))
-                                    (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
-            nat)
-  (nat-test (∅ n : nat)
-    (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n)
-    nat)
-  (check-holds
-    (type-check (,Δ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
-                (∅ n2 : nat)
-                (((((elim nat (Unv 0)) (λ (x : nat) bool))
-                   btrue)
-                  (λ (x : nat) (λ (ih-x : bool) bfalse)))
-                 n2)
-                bool))
-  (check-not-holds
-    (type-check ,Δ ∅
-             ((((elim nat (Unv 0)) nat) (s zero)) zero)
-                nat))
-  (define lam (term (λ (nat : (Unv 0)) nat)))
-  (check-equivalent
-    (Π (nat : (Unv 0)) (Unv 0))
-    ,(car (judgment-holds (type-infer ,Δ0 ∅ ,lam t) t)))
-  (check-equivalent
-    (Π (nat : (Unv 0)) (Unv 0))
-    ,(car (judgment-holds (type-infer ,Δ ∅ ,lam t) t)))
-  (check-equivalent
-    (Π (x : (Π (y : (Unv 0)) y)) nat)
-    ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
-                                  t) t)))
-  (check-equivalent
-    (Π (y : (Unv 0)) (Unv 0))
-    ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (y : (Unv 0)) y) t) t)))
-  (check-equivalent
-    (Unv 0)
-    ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅
-                                 ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
-                                  (λ (y : (Unv 0)) y))
-                                 t) t)))
-  (check-equal?
-    (list (term (Unv 0)) (term (Unv 1)))
-    (judgment-holds
-      (type-infer ,Δ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))
-                  U) U))
-  (check-holds
-    (type-check ,Δ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))
-  (check-holds
-    (type-check ,Δ4 (∅ S : (Unv 0))
-                conj (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : P) (Π (y : Q) ((and P) Q)))))))
-  (check-holds
-    (type-check ,Δ4 (∅ S : (Unv 0)) S (Unv 0)))
-  (check-holds
-    (type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
-                (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
-  (check-holds
-    (type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
-                (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
-  (check-holds
-    (type-check ,Δ4 ∅ (λ (S : (Unv 0)) (conj S))
-                (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
-  (check-holds
-    (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-                ((((conj true) true) tt) tt)
-                ((and true) true)))
-  (check-holds
-    (type-infer ,Δ4 ∅ and (in-hole Ξ U_D)))
-  (check-holds
-    (type-infer (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-                ((((conj true) true) tt) tt)
-                (in-hole Θ and)))
-  (check-holds
-    (type-infer (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-                (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
-                (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
-  (check-holds
-    (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             ((((((elim and (Unv 0))
-                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                 true))))
-                 (λ (A : (Unv 0))
-                    (λ (B : (Unv 0))
-                       (λ (a : A)
-                          (λ (b : B) tt)))))
-                true) true)
-              ((((conj true) true) tt) tt))
-                true))
-  (check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
-  (check-holds
-    (type-infer ,Δ4 ∅ and (in-hole Ξ U)))
-  (check-holds
-    (type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
-                ab (in-hole Θ and)))
-  (check-true
-    (redex-match? tt-redL
-                  (in-hole Ξ (Π (x : (in-hole Θ and)) U))
-                  (term (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0)))))))
-  (check-holds
-    (type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
-                (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                               ((and B) A))))
-                (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
-  (check-holds
-    (equivalent ,Δ4
-                (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))
-                (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0))))))
-  (check-holds
-    (type-infer ,Δ4 ∅
-                (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                               ((and B) A))))
-                (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
-  (check-holds
-    (type-check ,Δ4
-                (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
-             ((((((elim and (Unv 0))
-                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                 ((and B) A)))))
-                 (λ (A : (Unv 0))
-                    (λ (B : (Unv 0))
-                       (λ (a : A)
-                          (λ (b : B) ((((conj B) A) b) a))))))
-                P) Q) ab)
-                ((and Q) P)))
-  (check-holds
-    (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-                (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) ((and B) A))))
-                (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))))
-  (check-holds
-    (type-infer (,Δ4 (true : (Unv 0) ((tt : true))))
-                ((∅ A : Type) B : Type)
-                (conj B)
-                t))
-  (check-holds
-    (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             ((((((elim and (Unv 0))
-                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                 ((and B) A)))))
-                 (λ (A : (Unv 0))
-                    (λ (B : (Unv 0))
-                       (λ (a : A)
-                          (λ (b : B) ((((conj B) A) b) a))))))
-                true) true)
-              ((((conj true) true) tt) tt))
-                ((and true) true)))
-  (define gamma (term (∅ temp863 : pre)))
-  (check-holds (wf ,sigma ∅))
-  (check-holds (wf ,sigma ,gamma))
-  (check-holds
-    (type-infer ,sigma ,gamma (Unv 0) t))
-  (check-holds
-    (type-infer ,sigma ,gamma pre t))
-  (check-holds
-    (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
-  (check-holds
-    (type-infer ,sigma ,gamma pre t))
-  (check-holds
-    (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
-  (check-holds
-    (type-infer ,sigma (,gamma x : false) false (in-hole Ξ U_D)))
-  (check-holds
-    (type-infer ,sigma (,gamma x : false) x (in-hole Θ false)))
-  (check-holds
-    (type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
-                (in-hole Ξ (Π (x : (in-hole Θ false)) U))))
-  (check-true
-    (redex-match? tt-typingL
-                  ((in-hole Θ_m ((elim x_D U) e_P)) e_D)
-                  (term (((elim false (Unv 1)) (λ (y : false) (Π (x : Type) x)))
-                         x))))
-  (check-holds
-    (type-check ,sigma (,gamma x : false)
-                (((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x)
-                (Π (x : (Unv 0)) x)))
-
-  ;; nat-equal? tests
-  (define zero?
-    (term ((((elim nat Type) (λ (x : nat) bool))
-            true)
-           (λ (x : nat) (λ (x_ih : bool) false)))))
-  (check-holds
-    (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
-  (check-equal?
-    (term (reduce ,Δ (,zero? zero)))
-    (term true))
-  (check-equal?
-    (term (reduce ,Δ (,zero? (s zero))))
-    (term false))
-  (define ih-equal?
-    (term ((((elim nat Type) (λ (x : nat) bool))
-            false)
-           (λ (x : nat) (λ (y : bool) (x_ih x))))))
-  (check-holds
-    (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
-                ,ih-equal?
-                (Π (x : nat) bool)))
-  (check-holds
-    (type-infer ,Δ ∅ nat (Unv 0)))
-  (check-holds
-    (type-infer ,Δ ∅ bool (Unv 0)))
-  (check-holds
-    (type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
-  (define nat-equal?
-    (term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool)))
-            ,zero?)
-           (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
-                               ,ih-equal?)))))
-  (check-holds
-    (type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
-                                ((nat-equal? zero) zero)
-                bool))
-  (check-holds
-    (type-check ,Δ ∅
-                ,nat-equal?
-                (Π (x : nat) (Π (y : nat) bool))))
-  (check-equal?
-    (term (reduce ,Δ ((,nat-equal? zero) (s zero))))
-    (term false))
-  (check-equal?
-    (term (reduce ,Δ ((,nat-equal? (s zero)) zero)))
-    (term false))
-
-  ;; == tests
-  (define Δ= (term (,Δ (== : (Π (A : (Unv 0)) (Π (a : A) (Π (b : A) (Unv 0))))
-                             ((refl : (Π (A : (Unv 0)) (Π (a : A) (((== A) a) a)))))))))
-  (check-true (Δ? Δ=))
-
-  (define refl-elim
-    (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
-                                                                                              A1)
-                                                                                              x1)
-                                                                                             y1))
-                                                                                      nat)))))
-              (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))
-  (check-holds
-    (type-check ,Δ= ∅ ,refl-elim nat))
-  (check-true
-    (redex-match?
-      tt-redL
-      (Δ (in-hole E (in-hole Θ ((elim x_D U) e_P))))
-      (term (,Δ= ,refl-elim))))
-  (check-true
-    (redex-match?
-      tt-redL
-      (in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m)
-      (term (((((hole
-              (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true)))))
-  (check-telescope-equiv?
-    (term (Δ-ref-parameter-Ξ ,Δ= ==))
-    (term (Π (A : Type) (Π (a : A) (Π (b : A) hole)))))
-  (check-equal?
-    (term (reduce ,Δ= ,refl-elim))
-    (term zero)))
diff --git a/info.rkt b/info.rkt
deleted file mode 100644
index 7fc064f..0000000
--- a/info.rkt
+++ /dev/null
@@ -1,8 +0,0 @@
-#lang info
-(define collection "cur")
-(define deps '("base" "rackunit-lib" ("redex-lib" #:version "1.11")))
-(define build-deps '("scribble-lib" "racket-doc" "sandbox-lib"))
-(define scribblings '(("scribblings/cur.scrbl" (multi-page))))
-(define pkg-desc "Dependent types with parenthesis and meta-programming.")
-(define version "0.1")
-(define pkg-authors '(wilbowma))
diff --git a/stdlib/bool.rkt b/stdlib/bool.rkt
deleted file mode 100644
index 61cc897..0000000
--- a/stdlib/bool.rkt
+++ /dev/null
@@ -1,41 +0,0 @@
-#lang s-exp "../cur.rkt"
-(require "sugar.rkt")
-(provide Bool true false if not and or)
-
-(data Bool : Type
-  (true : Bool)
-  (false : Bool))
-
-(define-syntax-rule (if t s f)
-  (match t
-    [true s]
-    [false f]))
-
-(define (not (x : Bool)) (if x false true))
-
-(module+ test
-  (require rackunit)
-  (check-equal? (not true) false)
-  (check-equal? (not false) true))
-
-(define (and (x : Bool) (y : Bool))
-  (if x
-      y
-      (not y)))
-
-(module+ test
-  (check-equal? (and true false) false)
-  (check-equal? (and false false) true)
-  (check-equal? (and false true) false)
-  (check-equal? (and true true) true))
-
-(define (or (x : Bool) (y : Bool))
-  (if x
-      true
-      y))
-
-(module+ test
-  (check-equal? (or true false) true)
-  (check-equal? (or false false) false)
-  (check-equal? (or false true) true)
-  (check-equal? (or true true) true))
diff --git a/stdlib/maybe.rkt b/stdlib/maybe.rkt
deleted file mode 100644
index 2550871..0000000
--- a/stdlib/maybe.rkt
+++ /dev/null
@@ -1,29 +0,0 @@
-#lang s-exp "../cur.rkt"
-(require "sugar.rkt")
-(provide Maybe none some some/i)
-
-(data Maybe : (forall (A : Type) Type)
-  (none : (forall (A : Type) (Maybe A)))
-  (some : (forall* (A : Type) (a : A) (Maybe A))))
-
-(define-syntax (some/i syn)
-  (syntax-case syn ()
-   [(_ a)
-    (let ([a-ty (type-infer/syn #'a)])
-      #`(some #,a-ty a))]))
-
-(module+ test
-  (require rackunit "bool.rkt")
-  (check-equal?
-   (some/i true)
-   (some Bool true))
-  ;; Disabled until #22 fixed
-  #;(check-equal?
-    (case* Maybe Type (some Bool true) (Bool)
-      (lambda* (A : Type) (x : (Maybe A)) A)
-      [(none (A : Type)) IH: ()
-       false]
-      [(some (A : Type) (x : A)) IH: ()
-       ;; TODO: Don't know how to use dependency yet
-       (if x true false)])
-    true))