diff --git a/examples/stlc.rkt b/examples/stlc.rkt
index 0a1a570..4fa1e74 100644
--- a/examples/stlc.rkt
+++ b/examples/stlc.rkt
@@ -23,7 +23,7 @@
   (extend-gamma : (->* Gamma Var stlc-type Gamma)))
 
 (define (lookup-gamma (g : Gamma) (x : Var))
-  (case* Gamma g (lambda* (g : Gamma) (Maybe stlc-type))
+  (case* Gamma Type g () (lambda* (g : Gamma) (Maybe stlc-type))
     [emp-gamma (none stlc-type)]
     [(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
      IH: ((ih-g1 : (Maybe stlc-type)))
diff --git a/oll.rkt b/oll.rkt
index c20f82f..5bf13de 100644
--- a/oll.rkt
+++ b/oll.rkt
@@ -239,9 +239,9 @@
 (data Var : Type (avar : (-> Nat Var)))
 
 (define (var-equal? (v1 : Var) (v2 : Var))
-  (case* Var v1 (lambda (v : Var) Bool)
+  (case* Var Type v1 () (lambda (v : Var) Bool)
     [(avar (n1 : Nat)) IH: ()
-     (case* Var v2 (lambda (v : Var) Bool)
+     (case* Var Type v2 () (lambda (v : Var) Bool)
        [(avar (n2 : Nat)) IH: ()
         (nat-equal? n1 n2)])]))
 (module+ test
diff --git a/scribblings/curnel.scrbl b/scribblings/curnel.scrbl
index 9d80494..c9787cc 100644
--- a/scribblings/curnel.scrbl
+++ b/scribblings/curnel.scrbl
@@ -96,10 +96,11 @@ For instance, Cur does not currently perform strict positivity checking.
           ((((conj Bool) Bool) true) false)]
 }
 
-@defform[(elim type-expr expr motive method* ...)]{
-Eliminates the expression @racket[expr] of the inductively defined type @racket[type-expr], using
-@racket[motive], where the methods for each constructor for @racket[type-expr] are given by
-@racket[method*].
+@defform[(elim type motive-result-type)]{
+Returns the inductive eliminator for @racket[type] where the result type of the motive is
+@racket[motive-result-type]. The eliminator expects a motive, methods for each of the constructors of the
+inductive type @racket[type], parameters @racket[p ...] for the inductive @racket[type], and finally a
+type of @racket[(type p ...)].
 
 The following example runs @racket[(sub1 (s z))].
 
@@ -107,9 +108,11 @@ The following example runs @racket[(sub1 (s z))].
           (data Nat : Type
             (z : Nat)
             (s : (forall (n : Nat) Nat)))
-          (elim Nat (s z) (lambda (x : Nat) Nat)
-                z
-                (lambda (n : Nat) (lambda (IH : Nat) n)))]
+          (((((elim Nat Type)
+              (lambda (x : Nat) Nat))
+             z)
+            (lambda (n : Nat) (lambda (IH : Nat) n)))
+           (s z))]
 }
 
 @defform[(define id expr)]{
@@ -120,9 +123,9 @@ Binds @racket[id] to the result of @racket[expr].
             (z : Nat)
             (s : (forall (n : Nat) Nat)))
           (define sub1 (lambda (n : Nat)
-                         (elim Nat n (lambda (x : Nat) Nat)
-                               z
-                               (lambda (n : Nat) (lambda (IH : Nat) n)))))
+                         (((((elim Nat Type) (lambda (x : Nat) Nat))
+                           z)
+                          (lambda (n : Nat) (lambda (IH : Nat) n))) n)))
           (sub1 (s (s z)))
           (sub1 (s z))
           (sub1 z)]
diff --git a/scribblings/stdlib/sugar.scrbl b/scribblings/stdlib/sugar.scrbl
index 74f50d6..c6ef6cd 100644
--- a/scribblings/stdlib/sugar.scrbl
+++ b/scribblings/stdlib/sugar.scrbl
@@ -105,7 +105,7 @@ defined.
              false])]
 }
 
-@defform[(case* type e motive [pattern maybe-IH body] ...)
+@defform[(case* type motive-result-type e (parameters ...) motive [pattern maybe-IH body] ...)
          #:grammar
          [(pattern
             constructor
@@ -117,13 +117,20 @@ defined.
 A pattern-matcher-like syntax for inductive elimination that does not try to infer the type or motive.
 Necessary for more advanced types, like @racket[And], because @racket[case] is not very smart.
 
+@margin-note{Don't worry about all that output from requiring prop}
 @examples[#:eval curnel-eval
           (require cur/stdlib/nat)
-          (case* Nat z (lambda (x : Bool) Nat)
+          (case* Nat Type z () (lambda (x : Nat) Bool)
             [z true]
             [(s (n : Nat))
              IH: ((_ : Bool))
-             false])]
+             false])
+          (require cur/stdlib/prop)
+          (case* And Type (conj Bool Nat true z) (Bool Nat)
+            (lambda* (A : Type) (B : Type) (ab : (And A B)) A)
+            [(conj (A : Type) (B : Type) (a : A) (b : B))
+             IH: ()
+             a])]
 }
 
 @defform[(run syn)]{