diff --git a/cur-doc/cur/scribblings/curnel.scrbl b/cur-doc/cur/scribblings/curnel.scrbl
index 10283a1..2ff71fa 100644
--- a/cur-doc/cur/scribblings/curnel.scrbl
+++ b/cur-doc/cur/scribblings/curnel.scrbl
@@ -33,43 +33,44 @@ restricted impredicative universe.
           Type]
 }
 
-@defform*[((lambda (id : type-expr) body-expr)
-           (λ (id : type-expr) body-expr))]{
-Produces a single arity procedure, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr] and in the type of
-@racket[body-expr].
-Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms, such as macros.
+@defform[(λ (id : type-expr) body-expr)]{
+Produces a single-arity procedure, binding the identifier @racket[id] of type
+@racket[type-expr] in @racket[body-expr] and in the type of @racket[body-expr].
+Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms,
+such as macros.
 
-Currently, Cur will return the underlying representation of a procedure when a @racket[lambda] is
-evaluated at the top-level. Do not rely on this representation.
+Currently, Cur will return the underlying representation of a procedure when a
+@racket[λ] is evaluated at the top-level.
+Do not rely on this representation.
 
 @examples[#:eval curnel-eval
-          (lambda (x : Type) x)]
+          (λ (x : Type) x)]
 
 @examples[#:eval curnel-eval
-          (λ (x : Type) (lambda (y : x) y))]
+          (λ (x : Type) (λ (y : x) y))]
 
 
 @defform[(#%app procedure argument)]{
-Applies the single arity @racket[procedure] to @racket[argument].
+Applies the single-arity @racket[procedure] to @racket[argument].
 }
 
 @examples[#:eval curnel-eval
-          ((lambda (x : (Type 1)) x) Type)]
+          ((λ (x : (Type 1)) x) Type)]
 
 @examples[#:eval curnel-eval
-          (#%app (lambda (x : (Type 1)) x) Type)]
+          (#%app (λ (x : (Type 1)) x) Type)]
 }
 
-@defform*[((forall (id : type-expr) body-expr)
-           (∀ (id : type-expr) body-expr))]{
-Produces a dependent function type, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr].
+@defform[(Π (id : type-expr) body-expr)]{
+Produces a dependent function type, binding the identifier @racket[id] of type
+@racket[type-expr] in @racket[body-expr].
 
 
 @examples[#:eval curnel-eval
-          (forall (x : Type) Type)]
+          (Π (x : Type) Type)]
 
 @examples[#:eval curnel-eval
-          (lambda (x : (forall (x : (Type 1)) Type))
+          (λ (x : (Π (x : (Type 1)) Type))
             (x Type))]
 }
 
@@ -83,10 +84,10 @@ For instance, Cur does not currently perform strict positivity checking.
           (data Bool : Type
                 (true : Bool)
                 (false : Bool))
-          ((lambda (x : Bool) x) true)
+          ((λ (x : Bool) x) true)
           (data False : Type)
-          (data And : (forall (A : Type) (forall (B : Type) Type))
-            (conj : (forall (A : Type) (forall (B : Type) (forall (a : A) (forall (b : B) ((And A) B)))))))
+          (data And : (Π (A : Type) (Π (B : Type) Type))
+            (conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((And A) B)))))))
           ((((conj Bool) Bool) true) false)]
 }
 
@@ -103,11 +104,11 @@ The following example runs @racket[(sub1 (s z))].
 @examples[#:eval curnel-eval
           (data Nat : Type
             (z : Nat)
-            (s : (forall (n : Nat) Nat)))
+            (s : (Π (n : Nat) Nat)))
           (((((elim Nat Type)
-              (lambda (x : Nat) Nat))
+              (λ (x : Nat) Nat))
              z)
-            (lambda (n : Nat) (lambda (IH : Nat) n)))
+            (λ (n : Nat) (λ (IH : Nat) n)))
            (s z))]
 }
 
@@ -117,11 +118,11 @@ Binds @racket[id] to the result of @racket[expr].
 @examples[#:eval curnel-eval
           (data Nat : Type
             (z : Nat)
-            (s : (forall (n : Nat) Nat)))
-          (define sub1 (lambda (n : Nat)
-                         (((((elim Nat Type) (lambda (x : Nat) Nat))
+            (s : (Π (n : Nat) Nat)))
+          (define sub1 (λ (n : Nat)
+                         (((((elim Nat Type) (λ (x : Nat) Nat))
                            z)
-                          (lambda (n : Nat) (lambda (IH : Nat) n))) n)))
+                          (λ (n : Nat) (λ (IH : Nat) n))) n)))
           (sub1 (s (s z)))
           (sub1 (s z))
           (sub1 z)]
diff --git a/cur-doc/cur/scribblings/reflection.scrbl b/cur-doc/cur/scribblings/reflection.scrbl
index be97572..1fae978 100644
--- a/cur-doc/cur/scribblings/reflection.scrbl
+++ b/cur-doc/cur/scribblings/reflection.scrbl
@@ -25,8 +25,8 @@ phase 1 in Cur.}
 
 @examples[
 (eval:alts (define-syntax-rule (computed-type _) Type) (void))
-(eval:alts (cur-expand #'(lambda (x : (computed-type bla)) x))
-           (eval:result @racket[#'(lambda (x : Type) x)] "" ""))
+(eval:alts (cur-expand #'(λ (x : (computed-type bla)) x))
+           (eval:result @racket[#'(λ (x : Type) x)] "" ""))
 ]
 }
 
@@ -35,8 +35,8 @@ phase 1 in Cur.}
 Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred.
 
 @examples[
-(eval:alts (type-infer/syn #'(lambda (x : Type) x))
-           (eval:result @racket[#'(forall (x : (Type 0)) (Type 0))] "" ""))
+(eval:alts (type-infer/syn #'(λ (x : Type) x))
+           (eval:result @racket[#'(Π (x : (Type 0)) (Type 0))] "" ""))
 (eval:alts (type-infer/syn #'Type)
            (eval:result @racket[#'(Type 1)] "" ""))
 ]
@@ -47,7 +47,7 @@ Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could b
 Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise.
 
 @examples[
-(eval:alts (type-check/syn? #'(lambda (x : Type) x))
+(eval:alts (type-check/syn? #'(λ (x : Type) x))
            (eval:result @racket[#t] "" ""))
 (eval:alts (type-check/syn? #'Type)
            (eval:result @racket[#t] "" ""))
@@ -61,7 +61,7 @@ Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] o
 Runs the Cur term @racket[syn] to a value.
 
 @examples[
-(eval:alts (normalize/syn #'((lambda (x : Type) x) Bool))
+(eval:alts (normalize/syn #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
 (eval:alts (normalize/syn #'(sub1 (s (s z))))
            (eval:result @racket[#'(s z)] "" ""))
@@ -73,12 +73,12 @@ Runs the Cur term @racket[syn] to a value.
 Runs the Cur term @racket[syn] for one step.
 
 @examples[
-(eval:alts (step/syn #'((lambda (x : Type) x) Bool))
+(eval:alts (step/syn #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
 (eval:alts (step/syn #'(sub1 (s (s z))))
            (eval:result @racket[#'(((((elim Nat (Type 0))
-                                      (lambda (x2 : Nat) Nat)) z)
-                                    (lambda (x2 : Nat) (lambda (ih-n2 : Nat) x2)))
+                                      (λ (x2 : Nat) Nat)) z)
+                                    (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
                                    (s (s z)))] "" ""))
 ]
 }
@@ -90,11 +90,11 @@ equal modulo α and β-equivalence.
 @examples[
 
 
-(eval:alts (cur-equal? #'(lambda (a : Type) a) #'(lambda (b : Type) b))
+(eval:alts (cur-equal? #'(λ (a : Type) a) #'(λ (b : Type) b))
            (eval:result @racket[#t] "" ""))
-(eval:alts (cur-equal? #'((lambda (a : Type) a) Bool) #'Bool)
+(eval:alts (cur-equal? #'((λ (a : Type) a) Bool) #'Bool)
            (eval:result @racket[#t] "" ""))
-(eval:alts (cur-equal? #'(lambda (a : Type) (sub1 (s z))) #'(lambda (a : Type) z))
+(eval:alts (cur-equal? #'(λ (a : Type) (sub1 (s z))) #'(λ (a : Type) z))
            (eval:result @racket[#f] "" ""))
 ]
 }
@@ -106,7 +106,7 @@ Converts @racket[s] to a datum representation of the @tech{curnel form}, after e
 @examples[
 
 
-(eval:alts (cur-?datum #'(lambda (a : Type) a))
+(eval:alts (cur->datum #'(λ (a : Type) a))
            (eval:result @racket['(λ (a : (Unv 0) a))] "" ""))
 ]
 }
diff --git a/cur-doc/cur/scribblings/stdlib/sugar.scrbl b/cur-doc/cur/scribblings/stdlib/sugar.scrbl
index 685def1..8ac3e75 100644
--- a/cur-doc/cur/scribblings/stdlib/sugar.scrbl
+++ b/cur-doc/cur/scribblings/stdlib/sugar.scrbl
@@ -21,12 +21,15 @@ This library defines various syntactic extensions making Cur easier to write tha
 @defform*[((-> decl decl ... type)
            (→ decl decl ... type)
 	   (forall decl decl ... type)
-	   (∀ decl decl ... type))
+	   (∀ decl decl ... type)
+	   (Π decl decl ... type)
+	   (Pi decl decl ... type))
 	  #:grammar
 	  [(decl
 	     type
 	     (code:line (identifier : type)))]]{
 A multi-artiy function type that supports dependent and non-dependent type declarations and automatic currying.
+We provide lots of names for this form, because there are lots of synonyms in the literature.
 
 @examples[#:eval curnel-eval
           (data And : (-> Type Type Type)
diff --git a/cur-lib/cur/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt
index a66a954..ea67832 100644
--- a/cur-lib/cur/curnel/redex-lang.rkt
+++ b/cur-lib/cur/curnel/redex-lang.rkt
@@ -30,10 +30,10 @@
     [dep-provide provide]
     [dep-require require]
 
-    [dep-lambda lambda]
+    [dep-lambda λ]
     [dep-app #%app]
 
-    [dep-forall forall]
+    [dep-forall Π]
 
     [dep-inductive data]
 
diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt
index 9b80ced..bb064c2 100644
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@@ -5,7 +5,12 @@
   "stdlib/sugar.rkt"
   "stdlib/nat.rkt"
   ;; TODO: "real-"? More like "curnel-"
-  (only-in "cur.rkt" [#%app real-app] [elim real-elim] [forall real-forall] [lambda real-lambda]))
+  (only-in
+   "cur.rkt"
+   [#%app real-app]
+   [elim real-elim]
+   [Π real-forall]
+   [λ real-lambda]))
 
 (provide
   define-relation
diff --git a/cur-lib/cur/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt
index 659fc9b..dc42302 100644
--- a/cur-lib/cur/stdlib/sugar.rkt
+++ b/cur-lib/cur/stdlib/sugar.rkt
@@ -6,6 +6,8 @@
     [-> →]
     [-> forall]
     [-> ∀]
+    [-> Π]
+    [-> Pi]
     [lambda λ])
   #%app
   define
@@ -28,7 +30,8 @@
   (only-in "../cur.rkt"
     [elim real-elim]
     [#%app real-app]
-    [lambda real-lambda]
+    [λ real-lambda]
+    [Π real-Π]
     [define real-define]))
 
 (begin-for-syntax
@@ -51,7 +54,7 @@
     [(_ d:parameter-declaration ...+ result:result-type)
      (foldr (lambda (src name type r)
               (quasisyntax/loc src
-                (forall (#,name : #,type) #,r)))
+                (real-Π (#,name : #,type) #,r)))
             #'result
             (attribute d)
             (attribute d.name)
@@ -97,7 +100,7 @@
 (define-syntax define-type
   (syntax-rules ()
     [(_ (name (a : t) ...) body)
-     (define name (forall (a : t) ... body))]
+     (define name (-> (a : t) ... body))]
     [(_ name type)
      (define name type)]))
 
diff --git a/cur-lib/cur/stdlib/tactics/standard.rkt b/cur-lib/cur/stdlib/tactics/standard.rkt
index 0c1831b..a4c1f39 100644
--- a/cur-lib/cur/stdlib/tactics/standard.rkt
+++ b/cur-lib/cur/stdlib/tactics/standard.rkt
@@ -22,7 +22,7 @@
     [(forall (x:id : P:expr) body:expr)
      (let* ([ps (proof-state-extend-env ps name #'P)]
             [ps (proof-state-current-goal-set ps #'body)]
-            [ps (proof-state-fill-proof-hole ps (lambda (x) #`(lambda (#,name : P) #,x)))])
+            [ps (proof-state-fill-proof-hole ps (lambda (x) #`(λ (#,name : P) #,x)))])
        ps)]
     [_ (error 'intro "Can only intro when current goal is of the form (∀ (x : P) body)")]))