diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt
index f3451e9..cf7593c 100644
--- a/curnel/redex-lang.rkt
+++ b/curnel/redex-lang.rkt
@@ -53,13 +53,13 @@
   define-syntax
   begin-for-syntax
   define-for-syntax
-  (for-syntax (all-from-out syntax/parse))
   syntax-case
   syntax-rules
   define-syntax-rule
-  (for-syntax (all-from-out racket))
-  ;; reflection
   (for-syntax
+   (all-from-out syntax/parse)
+   (all-from-out racket)
+   (all-from-out racket/syntax)
     cur->datum
     cur-expand
     type-infer/syn
diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt
index 57694b1..f6bff06 100644
--- a/stdlib/nat.rkt
+++ b/stdlib/nat.rkt
@@ -15,18 +15,17 @@
   (check-equal? (add1 (s z)) (s (s z))))
 
 (define (sub1 (n : Nat))
-  (case n
+  (match n
     [z z]
-    [(s (x : Nat)) IH: ((ih-n : Nat)) x]))
+    [(s (x : Nat)) x]))
 (module+ test
   (check-equal? (sub1 (s z)) z))
 
 (define (plus (n1 : Nat) (n2 : Nat))
-  (case n1
+  (match n1
     [z n2]
     [(s (x : Nat))
-     IH: ((ih-n1 : Nat))
-     (s ih-n1)]))
+     (s (recur x))]))
 (module+ test
   (check-equal? (plus z z) z)
   (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
@@ -48,11 +47,10 @@
   (check-equal? (nat-equal? (s z) (s z)) true))
 
 (define (even? (n : Nat))
-  (elim Nat Type (lambda (x : Nat) Bool)
-        true
-        (lambda* (n : Nat) (odd? : Bool)
-           (not odd?))
-        n))
+  (match n
+    [z true]
+    [(s (n : Nat))
+     (not (recur n))]))
 
 (define (odd? (n : Nat))
   (not (even? n)))
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index 4802fac..f26b709 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -15,6 +15,8 @@
   define-type
   case
   case*
+  match
+  recur
   let
 
   ;; type-check
@@ -24,8 +26,7 @@
   run
   step
   step-n
-  query-type
-  )
+  query-type)
 
 (require
   (only-in "../cur.rkt"
@@ -33,7 +34,6 @@
     [#%app real-app]
     [define real-define]))
 
-
 (define-syntax (-> syn)
   (syntax-case syn ()
     [(_ t1 t2) #`(forall (#,(gensym) : t1) t2)]))
@@ -112,6 +112,67 @@
     [(_ D U e (p ...) P clause* ...)
      #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
 
+(begin-for-syntax
+  (define-struct clause (args body))
+  (define ih-dict (make-hash))
+  (define (clause-parse syn)
+    (syntax-case syn (:)
+      [((con (a : A) ...) body)
+       (make-clause #'((a : A) ...) #'body)]
+      [(e body)
+       (make-clause #'() #'body)]))
+
+  (define (infer-result clauses)
+    (for/or ([clause clauses])
+      (type-infer/syn (clause-body clause))))
+
+  (define (infer-ihs D motive args-syn)
+    (syntax-case args-syn (:)
+      [((a : A) ...)
+       (for/fold ([ih-dict (make-immutable-hash)])
+                 ([type-syn (syntax->list #'(A ...))]
+                  [arg-syn (syntax->list #'(a ...))]
+		 ;; NB: Non-hygenic
+		 #:when (cur-equal? type-syn D))
+         (dict-set ih-dict (syntax->datum arg-syn) `(,(format-id args-syn "ih-~a" arg-syn) . ,#`(#,motive #,arg-syn))))]
+      [() '()]))
+
+  (define (clause->method D motive clause)
+    (dict-clear! ih-dict)
+    (let* ([ihs (infer-ihs D motive (clause-args clause))]
+           [ih-args (dict-map
+                     ihs
+                     (lambda (k v)
+                       (dict-set! ih-dict k (car v))
+                       #`(#,(car v) : #,(cdr v))))])
+      #`(lambda* #,@(clause-args clause) #,@ih-args #,(clause-body clause)))))
+
+(define-syntax (recur syn)
+  (syntax-case syn ()
+    [(_ id)
+     (dict-ref
+      ih-dict
+      (syntax->datum #'id)
+      (lambda ()
+        (raise-syntax-error
+         'match
+         (format "Cannot recur on ~a" (syntax->datum #'id))
+         syn)))]))
+
+;; TODO: Test
+(define-syntax (match syn)
+  (syntax-case syn ()
+    [(_ e clause* ...)
+     (let* ([clauses (map clause-parse (syntax->list #'(clause* ...)))]
+            [R (infer-result clauses)]
+            [D (type-infer/syn #'e)]
+	    [motive #`(lambda (x : #,D) #,R)]
+            [U (type-infer/syn R)])
+       #`((elim #,D #,U)
+            #,motive
+	    #,@(map (curry clause->method D motive) clauses)
+	    e))]))
+
 (begin-for-syntax
   (define-syntax-class let-clause
     (pattern