diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt
index 13987f8..07fe348 100644
--- a/curnel/redex-lang.rkt
+++ b/curnel/redex-lang.rkt
@@ -174,14 +174,10 @@
                     [e (parameterize ([gamma (extend-Γ/term gamma x t)])
                          (cur->datum #'e))])
                (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-            [(elim t e P m ...)
-             (let* ([t (cur->datum #'t)]
-                    [e (cur->datum #'e)]
-                    [P (cur->datum #'P)]
-                    [e (term (((elim ,t) ,e) ,P))])
-               (for/fold ([e e])
-                         ([m (syntax->list #'(m ...))])
-                 (term (,e ,(cur->datum m)))))]
+            [(elim t1 t2)
+             (let* ([t1 (cur->datum #'t1)]
+                    [t2 (cur->datum #'t2)])
+               (term ((elim ,t1) ,t2)))]
             [(#%app e1 e2)
              (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
     (unless (and inner-expand? (type-infer/term reified-term))
@@ -414,10 +410,10 @@
        #'(void))]))
 
 (define-syntax (dep-elim syn)
-  (syntax-case syn (:)
-    [(_ D e P method ...)
+  (syntax-case syn ()
+    [(_ D T)
      (syntax->curnel-syntax
-       (quasisyntax/loc syn (elim D e P method ...)))]))
+       (quasisyntax/loc syn (elim D T)))]))
 
 ;; TODO: Not sure if this is the correct behavior for #%top
 (define-syntax (dep-top syn)
diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt
index 680b0cc..0e6491b 100644
--- a/stdlib/nat.rkt
+++ b/stdlib/nat.rkt
@@ -33,12 +33,12 @@
 
 ;; Credit to this function goes to Max
 (define nat-equal?
-  (elim Nat Type (lambda (x : Nat) (-> Nat Bool))
-    (elim Nat Type (lambda (x : Nat) Bool)
+  ((elim Nat Type) (lambda (x : Nat) (-> Nat Bool))
+    ((elim Nat Type) (lambda (x : Nat) Bool)
           true
           (lambda* (x : Nat) (ih-n2 : Bool) false))
     (lambda* (x : Nat) (ih : (-> Nat Bool))
-      (elim Nat Type (lambda (x : Nat) Bool)
+      ((elim Nat Type) (lambda (x : Nat) Bool)
             false
             (lambda* (x : Nat) (ih-bla : Bool)
                      (ih x))))))
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index 3bf88e7..66f87aa 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -88,13 +88,13 @@
      (let* ([D (type-infer/syn #'e)]
             [M (type-infer/syn (clause-body #'(clause* ...)))]
             [U (type-infer/syn M)])
-       #`(elim #,D U (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
+       #`((elim #,D #,U) (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
                e))]))
 
 (define-syntax (case* syn)
   (syntax-case syn ()
     [(_ D U e (p ...) P clause* ...)
-     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
+     #`((elim D U) P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
 
 (define-syntax-rule (define-theorem name prop)
   (define name prop))