diff --git a/stdlib/bool.rkt b/stdlib/bool.rkt
index dc05ed2..36a6823 100644
--- a/stdlib/bool.rkt
+++ b/stdlib/bool.rkt
@@ -9,9 +9,11 @@
   (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)))]))
+     (let* ([sty (type-infer/syn #'s)]
+            [M #`(lambda (x : #,(type-infer/syn #'t))
+                  #,sty)]
+            [U (type-infer/syn sty)])
+       (quasisyntax/loc syn (elim bool #,U #,M s f t)))]))
 
 (define (bnot (x : bool)) (if x bfalse btrue))
 (module+ test
diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt
index 6b2047d..2ae07b1 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 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 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)]))
@@ -32,17 +32,20 @@
 
 ;; Credit to this function goes to Max
 (define (nat-equal? (n1 : nat))
-  (elim nat n1 (lambda (x : nat) (-> nat bool))
-    (lambda (n2 : nat)
-      (elim nat n2 (lambda (x : nat) bool)
+  (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)))
+        (lambda* (x : nat) (ih-n2 : bool) bfalse)
+        b2))
     (lambda* (x : nat) (ih : (-> nat bool))
-      (lambda (n2 : nat)
-        (elim nat n2 (lambda (x : nat) bool)
+      (lambda (a2 : nat)
+        (elim nat Type (lambda (x : nat) bool)
           bfalse
           (lambda* (x : nat) (ih-bla : bool)
-            (ih x)))))))
+            (ih x))
+          a2)))
+    n1))
 (module+ test
   (check-equal? (nat-equal? z z) btrue)
   (check-equal? (nat-equal? z (s z)) bfalse)
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index 6959fcd..cb2a544 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 e P clause* ...)
-     #`(elim D e P #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
+    [(_ D U e P clause* ...)
+     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) e)]))
 
 (define-syntax-rule (define-theorem name prop)
   (define name prop))