diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt
index d815f6f..1ad58c0 100644
--- a/cur-lib/cur/curnel/redex-core.rkt
+++ b/cur-lib/cur/curnel/redex-core.rkt
@@ -27,10 +27,10 @@
   (i j k  ::= natural)
   (U ::= (Unv i))
   (D x c ::= variable-not-otherwise-mentioned)
-  (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) ...))))
+  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e)
+     ;; (elim inductive-type motive (indices ...) (methods ...) discriminant)
+     (elim D e (e ...) (e ...) e))
   #:binding-forms
   (λ (x : t) e #:refers-to x)
   (Π (x : t_0) t_1 #:refers-to x))
@@ -233,6 +233,11 @@
   [(list->Θ (e e_r ...))
    (in-hole (list->Θ (e_r ...)) (hole e))])
 
+(define-metafunction tt-ctxtL
+  apply : e e ... -> e
+  [(apply e_f e ...)
+   (in-hole (list->Θ (e ...)) e_f)])
+
 ;; 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
@@ -323,36 +328,6 @@
       (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.
 ;;
@@ -368,29 +343,40 @@
 ;; Ξ_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
+
+;; Returns the inductive hypotheses required for the elimination method of constructor c_i for
+;; inductive type D, when eliminating with motive t_P.
 (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))
+  Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
+  [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
+   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
+
+;; Returns the type of the method corresponding to c_i
+(define-metafunction tt-ctxtL
+  Δ-constructor-method-type : Δ D c t -> t
+  [(Δ-constructor-method-type Δ D c_i t_P)
+   (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a c_i))))
+   (where Θ_p (Δ-constructor-parameters Δ D c_i))
+   (where Ξ_a (Δ-constructor-telescope Δ D c_i))
+   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ D c_i t_P))])
+
+(define-metafunction tt-ctxtL
+  Δ-method-types : Δ D e -> (t ...)
+  [(Δ-method-types Δ D e)
+   ,(map (lambda (c) (term (Δ-constructor-method-type Δ D ,c e))) (term (c ...)))
+   (where (c ...) (Δ-ref-constructors Δ D))])
+
+(define-metafunction tt-ctxtL
+  Δ-motive-type : Δ D U -> t
+  [(Δ-motive-type Δ D U)
+   (in-hole Ξ_P*D U)
+   (where Ξ (Δ-ref-parameter-Ξ Δ D))
    ;; A fresh name to bind the discriminant
-   (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
+   (where x ,(variable-not-in (term (Δ 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))])
+   ;; of the indices and the inductive type applied to the
+   ;; indices
+   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ D)) hole)))])
 
 ;;; ------------------------------------------------------------------------
 ;;; Dynamic semantics
@@ -398,16 +384,21 @@
 ;;; 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)))
+  (v  ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
+  (Θv ::= hole (Θv v))
+  (C-elim  ::= (elim D t_P (e_i ...) (e_m ...) hole))
+  ;; call-by-value
+  (E  ::= hole (E e) (v E)
+      (elim D e (e ...) (v ... E e ...) e)
+      (elim D e (e ...) (v ...) E)
+      ;; reduce under Π (helps with typing checking)
+      ;; TODO: Should be done in conversion judgment
+      (Π (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))
+
 #|
  | The elim form must appear applied like so:
  | (elim D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
@@ -423,75 +414,6 @@
  |
  | Using contexts, this appears as (in-hole Θ ((elim D U) v_P))
  |#
-
-
-;;; NB: Next 3 meta-function Assume of Θ n constructors, j parameters, n+j+1-th element is discriminant
-
-;; Given the apply context Θ in which an elimination of D with motive
-;; v of type U appears, extract the parameters p ... from Θ.
-(define-metafunction tt-redL
-  elim-parameters : Δ D Θ -> Θ
-  [(elim-parameters Δ D Θ)
-    ;; Drop the methods, take the parameters
-   (list->Θ
-    ,(take
-      (drop (term (Θ->list Θ)) (term (Δ-constructor-count Δ D)))
-      (term (Δ-parameter-count Δ D))))])
-
-;; Given the apply context Θ in which an elimination of D with motive
-;; v of type U appears, extract the methods m_0 ... m_n from Θ.
-(define-metafunction tt-redL
-  elim-methods : Δ D Θ -> Θ
-  [(elim-methods Δ D Θ)
-   ;; Take the methods, one for each constructor
-   (list->Θ
-    ,(take
-      (term (Θ->list Θ))
-      (term (Δ-constructor-count Δ D))))])
-
-;; Given the apply context Θ in which an elimination of D with motive
-;; v of type U appears, extract the discriminant (c_i a ...) from Θ.
-(define-metafunction tt-redL
-  elim-discriminant : Δ D Θ -> e
-  [(elim-discriminant Δ D Θ)
-   ;; Drop the methods, the parameters, and take the last element
-   ,(car
-     (drop
-      (drop (term (Θ->list Θ)) (term (Δ-constructor-count Δ D)))
-      (term (Δ-parameter-count Δ D))))])
-
-;; Check that Θ is valid and ready to be evaluated as the arguments to an elim.
-;; has length m = n + j + 1 and D has n constructors and j parameters,
-;; and the 1 represents the discriminant.
-;; discharges assumption for previous 3 meta-functions
-(define-metafunction tt-redL
-  Θ-valid : Δ D Θ -> #t or #f
-  [(Θ-valid Δ D Θ)
-   #t
-   (where natural_m (Θ-length Θ))
-   (where natural_n (Δ-constructor-count Δ D))
-   (where natural_j (Δ-parameter-count Δ D))
-   (side-condition (= (+ (term natural_n) (term natural_j) 1) (term natural_m)))
-   ;; As Cur allows reducing (through reflection) open terms, 
-   ;; check that the discriminant is a canonical form so that
-   ;; reduction can proceed; otherwise not valid.
-   (where (in-hole Θ_i c_i) (elim-discriminant Δ D Θ))
-   (where D (Δ-key-by-constructor Δ c_i))]
-  [(Θ-valid Δ D Θ) #f])
-
-(module+ test
-  (require rackunit)
-  (check-equal?
-   (term (Θ-length (((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))
-   3)
-  (check-true
-   (term
-    (Θ-valid
-     ((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat))))) (bool : (Unv 0) ((true : bool) (false : bool))))
-     nat
-     (((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))))
-
-
 (define-metafunction tt-ctxtL
   is-inductive-argument : Δ D t -> #t or #f
   ;; Think this only works in call-by-value. A better solution would
@@ -505,39 +427,35 @@
 ;; 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)
 ;; TODO TTEESSSSSTTTTTTTT
-(define-metafunction tt-ctxtL
-  Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
+(define-metafunction tt-redL
+  Δ-inductive-elim : Δ D C-elim Θ -> Θ
   ;; NB: If metafunction fails, recursive
   ;; NB: elimination will be wrong. This will introduced extremely sublte bugs,
   ;; NB: inconsistency, failure of type safety, and other bad things.
   ;; NB: It should be tested and audited thoroughly
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
-   ((Δ-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 (term (is-inductive-argument Δ x_D t_i)))]
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
-   (Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)]
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m hole)
-   hole])
+  [(Δ-inductive-elim any ... hole)
+   hole]
+  [(Δ-inductive-elim Δ D C-elim (Θ_c t_i))
+   ((Δ-inductive-elim Δ D C-elim Θ_c)
+    (in-hole C-elim t_i))
+   (side-condition (term (is-inductive-argument Δ D t_i)))]
+  [(Δ-inductive-elim any ... (Θ_c t_i))
+   (Δ-inductive-elim any ... Θ_c)])
 
 (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 D U) v_P))))
-         (Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
-         ;; Check that Θv is valid to avoid capturing other things
-         (side-condition (term (Θ-valid Δ D Θv)))
-          ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
-          ;; the discriminant: the constructor c_i applied to its argument Θv_i
-         (where Θv_p (elim-parameters Δ D Θv))
-         (where Θv_m (elim-methods Δ D Θv))
-         (where (in-hole Θv_i c_i) (elim-discriminant Δ D Θv))
-         ;; Find the method for constructor x_ci, relying on the order of the arguments.
-         (where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ D c_i)))
+    (--> (Δ (in-hole E (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c))))
+         (Δ (in-hole E (in-hole Θ_mi v_mi)))
+         ;; Find the method for constructor c_i, relying on the order of the arguments.
+         (where natural (Δ-constructor-index Δ D c))
+         (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
          ;; Generate the inductive recursion
-         (where Θ_r (Δ-inductive-elim Δ D U v_P Θv_p Θv_m Θv_i))
+         #;(Δ-inductive-elim Δ D U v_P Θv_p Θv_m Θv_i)
+         (where Θ_ih (Δ-inductive-elim Δ D (elim D e_motive (e_i ...) (v_m ...) hole) Θv_c))
+         (where Θ_mi (in-hole Θ_ih Θv_c))
          -->elim)))
 
 (define-metafunction tt-redL
@@ -698,10 +616,16 @@
    ----------------- "DTR-Application"
    (type-infer Δ Γ (e_0 e_1) t_3)]
 
-  [(where t (Δ-elim-type Δ D U))
-   (type-infer Δ Γ t U_e)
+  [(type-check Δ Γ e_c (apply D e_i ...))
+
+   (type-infer Δ Γ e_motive (name t_motive (in-hole Ξ U)))
+   (convert Δ Γ t_motive (Δ-motive-type Δ D U))
+
+   (where (t_m ...) (Δ-method-types Δ D e_motive))
+   (type-check Δ Γ e_m t_m) ...
    ----------------- "DTR-Elim_D"
-   (type-infer Δ Γ (elim D U) t)])
+   (type-infer Δ Γ (elim D e_motive (e_i ...) (e_m ...) e_c)
+               (apply e_motive e_i ... e_c))])
 
 (define-judgment-form tt-typingL
   #:mode (type-check I I I I)
diff --git a/cur-test/cur/tests/redex-core.rkt b/cur-test/cur/tests/redex-core.rkt
index 52ad81d..067a51c 100644
--- a/cur-test/cur/tests/redex-core.rkt
+++ b/cur-test/cur/tests/redex-core.rkt
@@ -121,35 +121,10 @@
         (Π (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
 ;; ------------------------------------------------------------------------
@@ -157,21 +132,32 @@
 (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)))))
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
                          (hole zero)))
- (term (hole (((((elim nat Type) (λ (x : nat) nat))
-                (s zero))
-               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-              zero))))
+ (term (hole (elim nat (λ (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)))))
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
                          (hole (s zero))))
- (term (hole (((((elim nat Type) (λ (x : nat) nat))
-                (s zero))
-               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-              (s zero)))))
+ (term (hole (elim nat (λ (x : nat) nat) ()
+                   ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                   (s zero)))))
+(check-telescope-equiv?
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
+                         hole))
+ (term hole))
 
 ;; Tests for dynamic semantics
 ;; ------------------------------------------------------------------------
@@ -179,6 +165,8 @@
 (check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
 (check-true (v? (term (refl Nat))))
 (check-true (v? (term ((refl Nat) z))))
+(check-true (v? (term zero)))
+(check-true (v? (term (s zero))))
 
 ;; TODO: Move equivalence up here, and use in these tests.
 (check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
@@ -188,60 +176,68 @@
                   (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)))
+
+(check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0)
+(check-equiv? (term (reduce ,Δ (elim nat (λ (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))))
+(check-equiv? (term (reduce ,Δ (elim nat (λ (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)))))
+(check-equiv? (term (reduce ,Δ (elim nat (λ (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)))))
+               (elim nat (λ (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)))))
+             (elim nat (λ (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)))))
+   (elim nat (λ (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))))))
+                       (elim nat (λ (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)))))
+    (elim nat (λ (x : nat) nat)
+          ()
+          ((s (s zero))
+           (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+          zero)))))
 
 (define-syntax-rule (check-equivalent e1 e2)
   (check-holds (convert ∅ ∅ e1 e2)))
@@ -343,28 +339,42 @@
                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))))
+(check-equiv?
+ (term (Δ-motive-type ,Δtruth truth (Unv 2)))
+ (term (Π (x : truth) (Unv 2))))
+
+
+(check-holds (type-check ,Δtruth ∅ (Unv 0) ,(car (term (Δ-method-types ,Δtruth truth (λ (x : truth) (Unv 1)))))))
+
+(check-holds (type-check ,Δtruth ∅ (λ (x : truth) (Unv 1)) (Π (x : truth) (Unv 2))))
+
+(check-equiv?
+ (term (apply (λ (x : truth) (Unv 1)) T))
+ (term ((λ (x : truth) (Unv 1)) T)))
+
+(check-holds
+ (convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
+
+(check-holds (type-infer ,Δtruth
                          ∅
-                         ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
-                          T)
+                         (elim truth (λ (x : truth) (Unv 1))
+                               () ((Unv 0)) T)
+                         t))
+
+(check-holds (type-check ,Δtruth
+                         ∅
+                         (elim truth (λ (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)
+                             (elim truth Type () (Type) T)
                              (Unv 1)))
 (check-holds
  (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
@@ -382,47 +392,54 @@
   (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-test ∅ (elim nat (λ (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)))
+ (type-infer ,Δ ∅ (λ (x : nat)
+                    (elim nat (λ (x : nat) nat)
+                          ()
+                          (zero
+                           (λ (x : nat) (λ (ih-x : nat) x)))
+                          x))
              t))
-(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
-               zero)
-              (λ (x : nat) (λ (ih-x : nat) x)))
-             zero)
+(nat-test ∅ (elim nat (λ (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-test ∅ (elim nat (λ (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-test ∅ (elim nat (λ (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)
+          (elim nat (λ (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)
+             (elim nat (λ (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)
+             (elim nat nat () ((s zero)) zero)
              nat))
 (define lam (term (λ (nat : (Unv 0)) nat)))
 (check-equivalent
@@ -481,15 +498,15 @@
              (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))
+             (elim and
+                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                 true)))
+                   (true true)
+                   ((λ (A : (Unv 0))
+                      (λ (B : (Unv 0))
+                        (λ (a : A)
+                          (λ (b : B) tt)))))
+                   ((((conj true) true) tt) tt))
              true))
 (check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
 (check-holds
@@ -518,14 +535,15 @@
 (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)
+             (elim and
+                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                 ((and B) A))))
+                   (P Q)
+                   ((λ (A : (Unv 0))
+                      (λ (B : (Unv 0))
+                        (λ (a : A)
+                          (λ (b : B) ((((conj B) A) b) a))))))
+                   ab)
              ((and Q) P)))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
@@ -538,14 +556,14 @@
              t))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             ((((((elim and (Unv 0))
+             (elim and
                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                ((and B) A)))))
-                 (λ (A : (Unv 0))
+                                                ((and B) A))))
+                 (true true)
+                 ((λ (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)))
@@ -568,21 +586,18 @@
 (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)
+             (elim false (λ (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)))))
+  (term (λ (n : nat)
+          (elim nat (λ (x : nat) bool) ()
+              (true (λ (x : nat) (λ (x_ih : bool) false)))
+              n))))
 (check-holds
  (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
 (check-equal?
@@ -592,9 +607,12 @@
  (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))))))
+  (term (λ (ih : nat)
+          (elim nat (λ (x : nat) bool)
+              ()
+              (false
+               (λ (x : nat) (λ (y : bool) (x_ih x))))
+              ih))))
 (check-holds
  (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
              ,ih-equal?
@@ -606,10 +624,13 @@
 (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?)))))
+  (term (λ (n : nat)
+          (elim nat (λ (x : nat) (Π (x : nat) bool))
+              ()
+              (,zero?
+              (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+                             ,ih-equal?)))
+              n))))
 (check-holds
  (type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
              ((nat-equal? zero) zero)
@@ -631,19 +652,12 @@
 (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))))
+  (term (elim == (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) nat))))
+                  (bool true true)
+                  ((λ (A1 : (Unv 0)) (λ (x1 : A1) zero)))
+                  ((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