diff --git a/scribblings/stdlib/sugar.scrbl b/scribblings/stdlib/sugar.scrbl
index 4c97775..55eb301 100644
--- a/scribblings/stdlib/sugar.scrbl
+++ b/scribblings/stdlib/sugar.scrbl
@@ -83,7 +83,7 @@ defining curried functions via @racket[lambda*].
 Like @racket[define], but uses @racket[forall*] instead of @racket[lambda*].
 }
 
-@defform[(case* D e P [pattern maybe-IH body] ...)
+@defform[(case* e [pattern maybe-IH body] ...)
          #:grammar
          [(pattern
             constructor
@@ -98,7 +98,7 @@ defined.
 
 @examples[#:eval curnel-eval
           (require cur/stdlib/nat)
-          (case* Nat z (lambda (x : Nat) Bool)
+          (case z
             [z true]
             [(s (n : Nat))
              IH: ((_ : Bool))
diff --git a/stdlib/bool.rkt b/stdlib/bool.rkt
index 7e2c810..d0709a7 100644
--- a/stdlib/bool.rkt
+++ b/stdlib/bool.rkt
@@ -6,13 +6,10 @@
   (true : Bool)
   (false : Bool))
 
-(define-syntax (if syn)
-  (syntax-case syn ()
-    [(_ t s f)
-     ;; Compute the motive
-     (let ([M #`(lambda (x : #,(type-infer/syn #'t))
-                  #,(type-infer/syn #'s))])
-       (quasisyntax/loc syn (elim Bool t #,M s f)))]))
+(define-syntax-rule (if t s f)
+  (case t
+    [true s]
+    [false f]))
 
 (define (not (x : Bool)) (if x false true))
 
diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt
index d5df010..044166e 100644
--- a/stdlib/nat.rkt
+++ b/stdlib/nat.rkt
@@ -15,16 +15,17 @@
   (check-equal? (add1 (s z)) (s (s z))))
 
 (define (sub1 (n : Nat))
-  (case* Nat n (lambda (x : Nat) Nat)
+  (case n
     [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 n1 (lambda (x : Nat) Nat)
+  (case n1
     [z n2]
-    [(s (x : Nat)) IH: ((ih-n1 : Nat))
+    [(s (x : Nat))
+     IH: ((ih-n1 : Nat))
      (s ih-n1)]))
 (module+ test
   (check-equal? (plus z z) z)
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index 9391f48..cd0d35b 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -6,12 +6,8 @@
   lambda*
   #%app
   define
-  case*
-  define-type
-  define-theorem
-  qed
-  real-app
-  define-rec)
+  case
+  define-type)
 
 (require
   (only-in "../cur.rkt"
@@ -79,10 +75,17 @@
 
 ;; TODO: Expects clauses in same order as constructors as specified when
 ;; TODO: inductive D is defined.
-(define-syntax (case* syn)
-  (syntax-case syn ()
-    [(_ D e P clause* ...)
-     #`(elim D e P #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
+(define-syntax (case syn)
+  ;; duplicated code
+  (define (clause-body syn)
+    (syntax-case (car (syntax->list syn)) (: IH:)
+      [((con (a : A) ...) IH: ((x : t) ...) body) #'body]
+      [(e body) #'body]))
+  (syntax-case syn (=>)
+    [(_ e clause* ...)
+     (let* ([D (type-infer/syn #'e)]
+            [M (type-infer/syn (clause-body #'(clause* ...)))])
+       #`(elim #,D e (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))))]))
 
 (define-syntax-rule (define-theorem name prop)
   (define name prop))