diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt
index c4ce123..dc4aa06 100644
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@@ -4,7 +4,8 @@
 (require
   "stdlib/sugar.rkt"
   "stdlib/nat.rkt"
-  (only-in "cur.rkt" [#%app real-app] [elim real-elim]))
+  ;; TODO: "real-"? More like "curnel-"
+  (only-in "cur.rkt" [#%app real-app] [elim real-elim] [forall real-forall] [lambda real-lambda]))
 
 (provide
   define-relation
@@ -38,8 +39,7 @@
               x*:expr ...
               line:dash lab:id
               (name:id y* ...))
-              #:with rule #'(lab : (forall* d ...
-                                     (->* x* ... (name y* ...))))
+              #:with rule #'(lab : (-> d ... x* ... (name y* ...)))
               ;; TODO: convert meta-vars such as e1 to e_1
               #:attr latex (format "\\inferrule~n{~a}~n{~a}"
                              (string-trim
@@ -62,7 +62,7 @@
      #:fail-unless (andmap (curry equal? (syntax->datum #'n))
                            (syntax->datum #'(rules.name ...)))
      "Mismatch between relation declared name and result of inference rule"
-      (let ([output #`(data n : (->* types* ... Type) rules.rule ...)])
+      (let ([output #`(data n : (-> types* ... Type) rules.rule ...)])
         ;; TODO: Pull this out into a separate function and test. Except
         ;; that might make using attritbutes more difficult.
         (when (attribute latex-file)
@@ -128,7 +128,7 @@
              #:attr arg-context #'())
     (pattern ((~var e (right-clause type)) (~var e* (right-clause type)) ...)
              #:attr name (fresh-name #'e.name)
-             #:attr clause-context #`(e.name : (->* #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
+             #:attr clause-context #`(e.name : (-> #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
                                                     #,(hash-ref (nts) type)))
              #:attr arg-context #`(#,@(flatten-args #'e.arg-context #'(e*.arg-context ...)))))
 
@@ -243,7 +243,7 @@
     (syntax-parse (cur-expand syn #'define #'begin)
        ;; TODO: Need to add these to a literal set and export it
        ;; Or, maybe overwrite syntax-parse
-       #:literals (lambda forall data real-app real-elim define begin Type)
+       #:literals (real-lambda real-forall data real-app real-elim define begin Type)
        [(begin e ...)
         (for/fold ([str ""])
                   ([e (syntax->list #'(e ...))])
@@ -266,10 +266,10 @@
                       (format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
                     (output-coq #'body)))
           "")]
-       [(lambda ~! (x:id (~datum :) t) body:expr)
+       [(real-lambda ~! (x:id (~datum :) t) body:expr)
         (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
                 (output-coq #'body))]
-       [(forall ~! (x:id (~datum :) t) body:expr)
+       [(real-forall ~! (x:id (~datum :) t) body:expr)
         (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
                 (output-coq #'body))]
        [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
diff --git a/cur-lib/cur/stdlib/prop.rkt b/cur-lib/cur/stdlib/prop.rkt
index ff55f6b..d70b69f 100644
--- a/cur-lib/cur/stdlib/prop.rkt
+++ b/cur-lib/cur/stdlib/prop.rkt
@@ -61,20 +61,20 @@
             [(conj (A : Type) (B : Type) (a : A) (b : B)) b])))
 
 #| TODO: Disabled until #22 fixed
-(data Or : (forall* (A : Type) (B : Type) Type)
-  (left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
-  (right : (forall* (A : Type) (B : Type) (b : B) (Or A B))))
+(data Or : (forall (A : Type) (B : Type) Type)
+  (left : (forall (A : Type) (B : Type) (a : A) (Or A B)))
+  (right : (forall (A : Type) (B : Type) (b : B) (Or A B))))
 
 (define-theorem thm:A-or-A
-  (forall* (A : Type) (o : (Or A A)) A))
+  (forall (A : Type) (o : (Or A A)) A))
 
 (define proof:A-or-A
-  (lambda* (A : Type) (c : (Or A A))
+  (lambda (A : Type) (c : (Or A A))
     ;; TODO: What should the motive be?
-    (elim Or Type (lambda* (A : Type) (B : Type) (c : (Or A B)) A)
-      (lambda* (A : Type) (B : Type) (a : A) a)
+    (elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A)
+      (lambda (A : Type) (B : Type) (a : A) a)
       ;; TODO: How do we know B is A?
-      (lambda* (A : Type) (B : Type) (b : B) b)
+      (lambda (A : Type) (B : Type) (b : B) b)
       A A c)))
 
 (qed thm:A-or-A proof:A-or-A)
diff --git a/cur-lib/cur/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt
index f16b166..5c8310f 100644
--- a/cur-lib/cur/stdlib/sugar.rkt
+++ b/cur-lib/cur/stdlib/sugar.rkt
@@ -31,7 +31,7 @@
     [elim real-elim]
     [#%app real-app]
     ;; Somehow, using real-lambda instead of _lambda causes weird import error
-    [lambda _lambda]
+    [lambda real-lambda]
     #;[forall real-forall]
     [define real-define]))
 
@@ -80,7 +80,7 @@
     [(_ d:argument-declaration ...+ body:expr)
      (foldr (lambda (src name type r)
               (quasisyntax/loc src
-                (_lambda (#,name : #,type) #,r)))
+                (real-lambda (#,name : #,type) #,r)))
             #'body
             (attribute d)
             (attribute d.name)
diff --git a/cur-test/cur/tests/olly.rkt b/cur-test/cur/tests/olly.rkt
index ea33ce5..1812caa 100644
--- a/cur-test/cur/tests/olly.rkt
+++ b/cur-test/cur/tests/olly.rkt
@@ -67,7 +67,7 @@
      "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
      (second (string-split t "\n"))))
   (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
-                               (lambda* (x : nat) (ih-x : nat) ih-x)
+                               (lambda (x : nat) (ih-x : nat) ih-x)
                                e))])
     (check-regexp-match
      "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
@@ -75,7 +75,7 @@
   (check-regexp-match
    "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
    (parameterize ([coq-defns ""])
-     (output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
+     (output-coq #'(define thm:plus-commutes (forall (n : nat) (m : nat)
                                                       (== nat (plus n m) (plus m n)))))
      (coq-defns)))
   (check-regexp-match
diff --git a/cur-test/cur/tests/stdlib/list.rkt b/cur-test/cur/tests/stdlib/list.rkt
index e305ca0..afda5a8 100644
--- a/cur-test/cur/tests/stdlib/list.rkt
+++ b/cur-test/cur/tests/stdlib/list.rkt
@@ -17,24 +17,24 @@
  (:: (cons Bool true (nil Bool)) (List Bool)))
 (check-equal?
  (void)
- (:: (lambda* (A : Type) (a : A)
+ (:: (lambda (A : Type) (a : A)
              (ih-a : (-> Nat (Maybe A))) 
              (n : Nat)
              (match n
                [z (some A a)]
                [(s (n-1 : Nat))
                 (ih-a n-1)]))
-    (forall* (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
+     (forall (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
              (n : Nat)
              (Maybe A))))
 (check-equal?
  (void)
- (:: (lambda* (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
+ (:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
 (check-equal?
  (void)
- (:: (elim List Type (lambda* (A : Type) (ls : (List A)) Nat)
+ (:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat)
           (lambda (A : Type) z)
-          (lambda* (A : Type) (a : A) (ls : (List A)) (ih : Nat)
+          (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
                    z)
           Bool
           (nil Bool))
@@ -43,7 +43,7 @@
 
 (check-equal?
  (void)
- (:: list-ref (forall (A : Type) (->* (List A) Nat (Maybe A)))))
+ (:: list-ref (forall (A : Type) (-> (List A) Nat (Maybe A)))))
 (check-equal?
  ((list-ref Bool (cons Bool true (nil Bool))) z)
  (some Bool true))
diff --git a/cur-test/cur/tests/stdlib/maybe.rkt b/cur-test/cur/tests/stdlib/maybe.rkt
index 4389a4c..5444667 100644
--- a/cur-test/cur/tests/stdlib/maybe.rkt
+++ b/cur-test/cur/tests/stdlib/maybe.rkt
@@ -11,8 +11,8 @@
  (some Bool true))
 ;; Disabled until #22 fixed
 #;(check-equal?
-   (case* Maybe Type (some Bool true) (Bool)
-          (lambda* (A : Type) (x : (Maybe A)) A)
+   (case Maybe Type (some Bool true) (Bool)
+          (lambda (A : Type) (x : (Maybe A)) A)
           [(none (A : Type)) IH: ()
            false]
           [(some (A : Type) (x : A)) IH: ()
diff --git a/cur-test/cur/tests/stdlib/prop.rkt b/cur-test/cur/tests/stdlib/prop.rkt
index a4a881a..ec90b0c 100644
--- a/cur-test/cur/tests/stdlib/prop.rkt
+++ b/cur-test/cur/tests/stdlib/prop.rkt
@@ -11,8 +11,8 @@
 (:: pf:proj1 thm:proj1)
 (:: pf:proj2 thm:proj2)
 (check-equal?
- (elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
-       (λ* (A : Type) (x : A) z)
+ (elim == Type (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
+       (λ (A : Type) (x : A) z)
        Bool
        true
        true
diff --git a/cur-test/cur/tests/stdlib/sugar.rkt b/cur-test/cur/tests/stdlib/sugar.rkt
index d52b356..abc7eee 100644
--- a/cur-test/cur/tests/stdlib/sugar.rkt
+++ b/cur-test/cur/tests/stdlib/sugar.rkt
@@ -5,19 +5,19 @@
 
 ;; TODO: Missing tests for match, others
 (check-equal?
- ((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
+ ((λ (x : (Type 1)) (y : (∀ (x : (Type 1)) (Type 1))) (y x))
   Type
   (λ (x : (Type 1)) x))
  Type)
 
 (check-equal?
- ((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
+ ((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
   Type
   (λ (x : (Type 1)) x))
  Type)
 
 (check-equal?
- ((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
+ ((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
   Type
   (λ (x : (Type 1)) x))
  Type)
diff --git a/cur-test/cur/tests/stdlib/typeclass.rkt b/cur-test/cur/tests/stdlib/typeclass.rkt
index a0e9ab8..9f6ce6c 100644
--- a/cur-test/cur/tests/stdlib/typeclass.rkt
+++ b/cur-test/cur/tests/stdlib/typeclass.rkt
@@ -8,7 +8,7 @@
  cur/stdlib/typeclass)
 
 (typeclass (Eqv (A : Type))
-           (equal? : (forall* (a : A) (b : A) Bool)))
+           (equal? : (forall (a : A) (b : A) Bool)))
 (impl (Eqv Bool)
       (define (equal? (a : Bool) (b : Bool))
         (if a
diff --git a/cur-test/cur/tests/stlc.rkt b/cur-test/cur/tests/stlc.rkt
index b459eed..f032be2 100644
--- a/cur-test/cur/tests/stlc.rkt
+++ b/cur-test/cur/tests/stlc.rkt
@@ -21,10 +21,10 @@
 ;; TODO: Abstract this over stlc-type, and provide from in OLL
 (data Gamma : Type
   (emp-gamma : Gamma)
-  (extend-gamma : (->* Gamma Var stlc-type Gamma)))
+  (extend-gamma : (-> Gamma Var stlc-type Gamma)))
 
 (define (lookup-gamma (g : Gamma) (x : Var))
-  (case* Gamma Type 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)))
@@ -97,7 +97,7 @@
          ;; Replace x with a de bruijn index, by running a CIC term at
          ;; compile time.
          (normalize/syn
-           #`((lambda* (x : stlc-term)
+           #`((lambda (x : stlc-term)
                       (stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
              (Var-->-stlc-term (avar #,oldindex)))))]
       [(quote (e1 e2))
@@ -106,7 +106,7 @@
        (let* ([y index]
               [x #`(s #,y)])
          (set! index #`(s (s #,index)))
-         #`((lambda* (x : stlc-term) (y : stlc-term)
+         #`((lambda (x : stlc-term) (y : stlc-term)
               (stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
                    #,(stlc #'e2)))
             (Var-->-stlc-term (avar #,x))