diff --git a/cur-lib/cur/curnel/redex-core-api.rkt b/cur-lib/cur/curnel/redex-core-api.rkt
index 4f09d74..9ea82ef 100644
--- a/cur-lib/cur/curnel/redex-core-api.rkt
+++ b/cur-lib/cur/curnel/redex-core-api.rkt
@@ -20,9 +20,9 @@
 (define Ξ? (redex-match? tt-ctxtL Ξ))
 (define Φ? (redex-match? tt-ctxtL Φ))
 (define Θ? (redex-match? tt-ctxtL Θ))
-(define Θv? (redex-match? tt-redL Θv))
-(define E? (redex-match? tt-redL E))
-(define v? (redex-match? tt-redL v))
+(define Θv? (redex-match? tt-cbvL Θv))
+(define E? (redex-match? tt-cbvL E))
+(define v? (redex-match? tt-cbvL v))
 
 (define-metafunction ttL
   subst-all : t (x ...) (e ...) -> t
diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt
index ad4b4ea..4d5cb21 100644
--- a/cur-lib/cur/curnel/redex-core.rkt
+++ b/cur-lib/cur/curnel/redex-core.rkt
@@ -29,6 +29,7 @@
   (D x c ::= variable-not-otherwise-mentioned)
   (Δ   ::= ∅ (Δ (D : t ((c : t) ...))))
   (t e ::= U (λ (x : e) e) x (Π (x : e) e) (e e)
+     ;; TODO: Might make more sense for methods to come first
      ;; (elim inductive-type motive (indices ...) (methods ...) discriminant)
      (elim D e (e ...) (e ...) e))
   #:binding-forms
@@ -243,22 +244,6 @@
       (hypotheses-loop D t_P Φ_1))
    (where x_h ,(variable-not-in (term (D t_P any_0)) 'x-ih))])
 
-;; Computes the type of the eliminator for the inductively defined type D with a motive whose result
-;; is in universe U.
-;;
-;; The type of (elim D U) is something like:
-;;  (∀ (P : (∀ a -> ... -> (D a ...) -> U))
-;;     (method_ci ...) -> ... ->
-;;     (a -> ... -> (D a ...) ->
-;;       (P a ... (D a ...))))
-;;
-;; 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 indices of D and
-;;       the witness of type D (applied to the indices)
-;; Ξ_m   is the telescope of the methods for 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
@@ -306,13 +291,7 @@
 ;;; inductively defined type x with a motive whose result is in universe U
 
 (define-extended-language tt-redL tt-ctxtL
-  (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)))
+  (C-elim  ::= (elim D t_P (e_i ...) (e_m ...) hole)))
 
 (define-metafunction tt-ctxtL
   is-inductive-argument : Δ_0 D_0 t -> #t or #f
@@ -372,7 +351,21 @@
            (where Θ_mi (in-hole Θ_ih Θ_c))
            -->elim))))
 
-(define (tt-->cbv D) (context-closure (tt--> D) tt-redL E))
+(define-extended-language tt-cbvL tt-redL
+  ;; NB: Not exactly right; only true when c is a constructor
+  (v  ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
+  (Θv ::= hole (Θv v))
+  (E  ::= hole (E e) (v E)
+      (elim D e (e ...) (v ... E e ...) e)
+      (elim D e (e ...) (v ...) E)))
+
+(define-extended-language tt-cbnL tt-cbvL
+  (E  ::= hole (E e) (elim D e (e ...) (e ...) E)))
+
+(define (tt-->cbv D) (context-closure (tt--> D) tt-cbvL E))
+;; Lazyness has lots of implications, such as on conversion and test suite.
+(define (tt-->cbn D) (context-closure (tt--> D) tt-cbnL E))
+;; Full reduction seems to loop forever
 (define (tt-->full D) (compatible-closure (tt--> D) tt-redL e))
 
 (define-metafunction tt-redL
@@ -430,6 +423,8 @@
   [(Γ-ref (Γ x_!_0 : t_0) (name x_1 x_!_0))
    (Γ-ref Γ x_1)])
 
+;; TODO: After reading https://coq.inria.fr/doc/Reference-Manual006.html#sec209, not convinced this is right.
+
 (define-metafunction tt-typingL
   nonpositive : x t -> #t or #f
   [(nonpositive x (in-hole Θ x))