diff --git a/oll.rkt b/oll.rkt
index c5536d1..70c2acb 100644
--- a/oll.rkt
+++ b/oll.rkt
@@ -4,7 +4,7 @@
 (require
   "stdlib/sugar.rkt"
   "stdlib/nat.rkt"
-  (only-in "curnel/redex-lang.rkt" [#%app real-app] [elim real-elim]))
+  (only-in "cur.rkt" [#%app real-app] [elim real-elim]))
 
 (provide
   define-relation
@@ -12,8 +12,7 @@
   Var
   avar
   var-equal?
-  generate-coq
-  #;(rename-out [oll-define-theorem define-theorem]))
+  generate-coq)
 
 (begin-for-syntax
   (define-syntax-class dash
@@ -275,31 +274,14 @@
         (string-replace str (symbol->string (first p))
                         (symbol->string (second p))))))
   (define (output-coq syn)
-    (syntax-parse (cur-expand syn #'define #'define-theorem #'qed
-                              #'begin)
+    (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-theorem
-                          define qed begin Type)
+       #:literals (lambda forall data real-app real-elim define begin Type)
        [(begin e ...)
         (for/fold ([str ""])
                   ([e (syntax->list #'(e ...))])
           (format "~a~n" (output-coq e)))]
-       [(define-theorem name prop)
-        (begin
-          (fprintf (current-error-port) "Warning: If theorem ~a is not followed by a proof using (qed ...), the resulting Coq code may be malformed.~n" (output-coq #'name))
-          (coq-lift-top-level
-            (format "Theorem ~a : ~a.~n"
-                    (output-coq #'name)
-                    (output-coq #'prop)))
-          "")]
-       [(qed thm proof)
-        ;; TODO: Have some sort of coq-lift-to-theorem, to auto match
-        ;; proofs and theorems.
-        (begin
-          (coq-lift-top-level
-            (format "Proof. exact ~a. Qed.~n" (output-coq #'proof)))
-          "")]
        [(define name:id body)
         (begin
           (coq-lift-top-level
@@ -392,10 +374,9 @@
         "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
         t))
     (check-regexp-match
-      "Theorem thm_plus_commutes : \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
+      "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
       (parameterize ([coq-defns ""])
-        (output-coq #'(define-theorem 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/scribblings/stdlib/sugar.scrbl b/scribblings/stdlib/sugar.scrbl
index 5936fa8..7f045cc 100644
--- a/scribblings/stdlib/sugar.scrbl
+++ b/scribblings/stdlib/sugar.scrbl
@@ -167,6 +167,15 @@ corresponding @racket[expr], raising a syntax error if no type can be inferred.
             (y x))]
 }
 
+@defform[(:: e type)]{
+Check that expression @racket[e] has type @racket[type], causing a type-error if not, and producing
+@racket[(void)] if so.
+
+@examples[#:eval curnel-eval
+          (:: z Nat)
+          (:: true Nat)]
+}
+
 @defform[(run syn)]{
 Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
 computing part of the term from another Cur term.
diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt
index a725f2a..81e05a6 100644
--- a/stdlib/prop.rkt
+++ b/stdlib/prop.rkt
@@ -5,20 +5,26 @@
 (provide
   True T
   thm:anything-implies-true
+  pf:anything-implies-true
   False
   Not
   And
   conj conj/i
-  thm:and-is-symmetric proof:and-is-symmetric
-  thm:proj1 proof:proj1
-  thm:proj2 proof:proj2
+  thm:and-is-symmetric pf:and-is-symmetric
+  thm:proj1 pf:proj1
+  thm:proj2 pf:proj2
   == refl)
 
+(module+ test
+  (require rackunit))
+
 (data True : Type (T : True))
 
-(define-theorem thm:anything-implies-true (forall (P : Type) True))
+(define thm:anything-implies-true (forall (P : Type) True))
+(define pf:anything-implies-true (lambda (P : Type) T))
 
-(qed thm:anything-implies-true (lambda (P : Type) T))
+(module+ test
+  (:: pf:anything-implies-true thm:anything-implies-true))
 
 (data False : Type)
 
@@ -35,39 +41,42 @@
            [b-type (type-infer/syn #'b)])
        #`(conj #,a-type #,b-type a b))]))
 
-(define-theorem thm:and-is-symmetric
+(define thm:and-is-symmetric
   (forall* (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
 
-(define proof:and-is-symmetric
+(define pf:and-is-symmetric
   (lambda* (P : Type) (Q : Type) (ab : (And P Q))
     (case* And Type ab (P Q)
       (lambda* (P : Type) (Q : Type) (ab : (And P Q))
          (And Q P))
       ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
 
-(qed thm:and-is-symmetric proof:and-is-symmetric)
+(module+ test
+  (:: pf:and-is-symmetric thm:and-is-symmetric))
 
-(define-theorem thm:proj1
+(define thm:proj1
   (forall* (A : Type) (B : Type) (c : (And A B)) A))
 
-(define proof:proj1
+(define pf:proj1
   (lambda* (A : Type) (B : Type) (c : (And A B))
     (case* And Type c (A B)
       (lambda* (A : Type) (B : Type) (c : (And A B)) A)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
-(qed thm:proj1 proof:proj1)
+(module+ test
+  (:: pf:proj1 thm:proj1))
 
-(define-theorem thm:proj2
+(define thm:proj2
   (forall* (A : Type) (B : Type) (c : (And A B)) B))
 
-(define proof:proj2
+(define pf:proj2
   (lambda* (A : Type) (B : Type) (c : (And A B))
     (case* And Type c (A B)
       (lambda* (A : Type) (B : Type) (c : (And A B)) B)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
-(qed thm:proj2 proof:proj2)
+(module+ test
+  (:: pf:proj2 thm:proj2))
 
 #| TODO: Disabled until #22 fixed
 (data Or : (forall* (A : Type) (B : Type) Type)
@@ -93,7 +102,7 @@
   (refl : (forall* (A : Type) (x : A) (== A x x))))
 
 (module+ test
-  (require rackunit "bool.rkt" "nat.rkt")
+  (require  "bool.rkt" "nat.rkt")
   (check-equal?
     (elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
          (λ* (A : Type) (x : A) z)
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index ef6250b..92dcfd5 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -17,15 +17,14 @@
   case*
   let
 
+  ;; type-check
+  ::
+
   ;; reflection in syntax
   run
   step
   step-n
   query-type
-
-  ;; don't use these
-  define-theorem
-  qed
   )
 
 (require
@@ -132,17 +131,19 @@
     [(let (c:let-clause ...) body)
      #'((lambda* (c.id : c.type) ... body) c.e ...)]))
 
-(define-syntax-rule (define-theorem name prop)
-  (define name prop))
-
-(define-syntax (qed stx)
-  (syntax-case stx ()
-    [(_ t pf)
+;; Normally type checking will only happen if a term is actually used. This forces a term to be
+;; checked against a particular type.
+(define-syntax (:: syn)
+  (syntax-case syn ()
+    [(_ pf t)
      (begin
        (unless (type-check/syn? #'pf #'t)
-         (raise-syntax-error 'qed "Invalid proof"
-           #'pf #'t))
-       #'pf)]))
+         (raise-syntax-error
+           '::
+           (format "Term ~a does not have expected type ~a. Inferred type was ~a"
+                   (cur->datum #'pf) (cur->datum #'t) (cur->datum (type-infer/syn #'pf)))
+           syn))
+       #'(void))]))
 
 (define-syntax (run syn)
   (syntax-case syn ()