diff --git a/redex-curnel.rkt b/redex-curnel.rkt
index 0fb8dd7..53ac7df 100644
--- a/redex-curnel.rkt
+++ b/redex-curnel.rkt
@@ -308,20 +308,27 @@
            -->β)
       (--> (Σ (in-hole E (in-hole Θ (((elim x_D) U) e_P))))
            (Σ (in-hole E (in-hole Θ_r (in-hole Θ_i e_mi))))
-           ;; The elim form must appear applied like so:
-           ;; (elim x_D U e_P m_0 ... m_i m_j ... m_n p ... (c_i p ... a ...))
-           ;; Where:
-           ;    x_D       is the inductive being eliminated
-           ;    U         is the sort of the motive
-           ;    e_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 non-parameter arguments to c_i
-           ;; Unfortunately, Θ contexts turn all this inside out:
-           ;; TODO: Write better abstractions for this notation
+           #|
+            |
+            | The elim form must appear applied like so:
+            | (elim x_D U e_P m_0 ... m_i m_j ... m_n p ... (c_i p ... a ...))
+            | -->
+            |
+            | Where:
+            |   x_D       is the inductive being eliminated
+            |   U         is the sort of the motive
+            |   e_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 non-parameter arguments to c_i
+            | Unfortunately, Θ contexts turn all this inside out:
+            | TODO: Write better abstractions for this notation
+            |#
            (where (in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m)
                   Θ)
+           (where Ξ (parameters-of Σ x_D))
+           (judgment-holds (telescope-types Σ ∅ Θ_p Ξ))
            (where (in-hole Θ_a Θ_p)
                   Θ_i)
            (where ((x_c* : t_c*) ...)
@@ -605,6 +612,15 @@
       (term (constructor-of ,Σ s))
       (term nat)))
 
+  ;; TODO: inlined at least in type-infer
+  ;; TODO: Define generic traversals of Σ and Γ ?
+  (define-metafunction cic-redL
+    parameters-of : Σ x -> Ξ
+    [(parameters-of (Σ (x_D : (in-hole Ξ U) ((x : t) ...))) x_D)
+     Ξ]
+    [(parameters-of (Σ (x_1 : t_1 ((x : t) ...))) x_D)
+     (parameters-of Σ x_D)])
+
   ;; Returns the constructors for the inductively defined type x_D in
   ;; the signature Σ
   (define-metafunction cic-redL
@@ -1011,10 +1027,10 @@
     (check-holds
       (type-check ,Σ ∅ ,zero? (Π (x : nat) bool)))
     (check-equal?
-      (term (reduce ,Σ (,zero? z)))
+      (term (reduce ,Σ (,zero? zero)))
       (term true))
     (check-equal?
-      (term (reduce ,Σ (,zero? (s z))))
+      (term (reduce ,Σ (,zero? (s zero))))
       (term false))
     (define ih-equal?
       (term (((((elim nat) Type) (λ (x : nat) bool))
@@ -1024,21 +1040,27 @@
       (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 ,Σ ∅
-                  (((((((elim nat) Type) (λ (x : nat) (Π (x : nat) bool)))
-                      ,zero?)
-                     (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
-                                         ,ih-equal?)))
-                    z) (s z))
+                  ,nat-equal?
                   (Π (x : nat) (Π (y : nat) bool))))
     (check-equal?
-      (term (reduce ,Σ (((((((elim nat) Type) (λ (x : nat) (Π (x : nat) bool)))
-                 ,zero?)
-                (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
-                                    ,ih-equal?)))
-               z) (s z))))
-      false)))
+      (term (reduce ,Σ ((,nat-equal? zero) (s zero))))
+      (term false))
+    (check-equal?
+      (term (reduce ,Σ ((,nat-equal? (s zero)) zero)))
+      (term false))))
 
 ;; This module just provide module language sugar over the redex model.
 
diff --git a/stdlib/maybe.rkt b/stdlib/maybe.rkt
index c8c3352..564017c 100644
--- a/stdlib/maybe.rkt
+++ b/stdlib/maybe.rkt
@@ -9,8 +9,8 @@
 (module+ test
   (require rackunit "bool.rkt")
   #;(check-equal?
-    (case* maybe (some bool btrue)
-      (lambda (x : (maybe bool)) bool)
+    (case* maybe Type (some bool btrue) (bool)
+      (lambda* (A : Type) (x : (maybe A)) A)
       [(none (A : Type)) IH: ()
        bfalse]
       [(some (A : Type) (x : A)) IH: ()
diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt
index 2ae07b1..5853d5d 100644
--- a/stdlib/nat.rkt
+++ b/stdlib/nat.rkt
@@ -15,14 +15,14 @@
   (check-equal? (add1 (s z)) (s (s z))))
 
 (define (sub1 (n : nat))
-  (case* nat Type n (lambda (x : nat) nat)
+  (case* nat Type n () (lambda (x : nat) nat)
     [z z]
     [(s (x : nat)) IH: ((ih-n : nat)) x]))
 (module+ test
   (check-equal? (sub1 (s z)) z))
 
 (define (plus (n1 : nat) (n2 : nat))
-  (case* nat Type n1 (lambda (x : nat) nat)
+  (case* nat Type n1 () (lambda (x : nat) nat)
     [z n2]
     [(s (x : nat)) IH: ((ih-n1 : nat))
      (s ih-n1)]))
@@ -31,21 +31,16 @@
   (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
 
 ;; Credit to this function goes to Max
-(define (nat-equal? (n1 : nat))
+(define nat-equal?
   (elim nat Type (lambda (x : nat) (-> nat bool))
-    (lambda (b2 : nat)
-      (elim nat Type (lambda (x : nat) bool)
-        btrue
-        (lambda* (x : nat) (ih-n2 : bool) bfalse)
-        b2))
+    (elim nat Type (lambda (x : nat) bool)
+          btrue
+          (lambda* (x : nat) (ih-n2 : bool) bfalse))
     (lambda* (x : nat) (ih : (-> nat bool))
-      (lambda (a2 : nat)
-        (elim nat Type (lambda (x : nat) bool)
-          bfalse
-          (lambda* (x : nat) (ih-bla : bool)
-            (ih x))
-          a2)))
-    n1))
+      (elim nat Type (lambda (x : nat) bool)
+            bfalse
+            (lambda* (x : nat) (ih-bla : bool)
+                     (ih x))))))
 (module+ test
   (check-equal? (nat-equal? z z) btrue)
   (check-equal? (nat-equal? z (s z)) bfalse)
diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt
index 8a7b36a..83db7c7 100644
--- a/stdlib/prop.rkt
+++ b/stdlib/prop.rkt
@@ -33,7 +33,7 @@
 
 (define proof:and-is-symmetric
   (lambda* (P : Type) (Q : Type) (ab : (and P Q))
-    (case* and ab
+    (case* and Type ab (P Q)
       (lambda* (P : Type) (Q : Type) (ab : (and P Q))
          (and Q P))
       ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj Q P y x)))))
@@ -45,7 +45,7 @@
 
 (define proof:proj1
   (lambda* (A : Type) (B : Type) (c : (and A B))
-    (case* and c
+    (case* and Type c (A B)
       (lambda* (A : Type) (B : Type) (c : (and A B)) A)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
@@ -56,7 +56,7 @@
 
 (define proof:proj2
   (lambda* (A : Type) (B : Type) (c : (and A B))
-    (case* and c
+    (case* and Type c (A B)
       (lambda* (A : Type) (B : Type) (c : (and A B)) B)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index cb2a544..5f19edf 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -78,8 +78,8 @@
 ;; TODO: inductive D is defined.
 (define-syntax (case* syn)
   (syntax-case syn ()
-    [(_ D U e P clause* ...)
-     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) e)]))
+    [(_ D U e (p ...) P clause* ...)
+     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
 
 (define-syntax-rule (define-theorem name prop)
   (define name prop))