diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt
index 393ce85..73f3c67 100644
--- a/turnstile/examples/exist.rkt
+++ b/turnstile/examples/exist.rkt
@@ -18,9 +18,9 @@
   [(pack (τ:type e) as ∃τ:type) ≫
    [#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm]
    [#:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)]
-   [⊢ [[e ≫ e-] ⇐ : τ_e]]
+   [⊢ [e ≫ e- ⇐ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : ∃τ.norm]]])
+   [⊢ [_ ≫ e- ⇒ : ∃τ.norm]]])
 
 (define-typed-syntax open #:datum-literals (<= with)
   [(open [x:id <= e_packed with X:id] e)
@@ -68,8 +68,8 @@
    ;; ------------------------------
    ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
    ;;
-   [⊢ [[e_packed ≫ e_packed-] ⇒ : (~∃ (Y) τ_body)]]
+   [⊢ [e_packed ≫ e_packed- ⇒ : (~∃ (Y) τ_body)]]
    [#:with τ_x (subst #'X #'Y #'τ_body)]
-   [([X : #%type ≫ X-]) ([x : τ_x ≫ x-]) ⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ [e ≫ e- ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ (let- ([x- e_packed-]) e-)] ⇒ : τ_e]]])
+   [⊢ [_ ≫ (let- ([x- e_packed-]) e-) ⇒ : τ_e]]])
diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt
index 1c85c82..39d6213 100644
--- a/turnstile/examples/ext-stlc.rkt
+++ b/turnstile/examples/ext-stlc.rkt
@@ -25,17 +25,17 @@
 (define-typed-syntax #%datum
   [(#%datum . b:boolean) ≫
    --------
-   [⊢ [[_ ≫ (#%datum- . b)] ⇒ : Bool]]]
+   [⊢ [_ ≫ (#%datum- . b) ⇒ : Bool]]]
   [(#%datum . s:str) ≫
    --------
-   [⊢ [[_ ≫ (#%datum- . s)] ⇒ : String]]]
+   [⊢ [_ ≫ (#%datum- . s) ⇒ : String]]]
   [(#%datum . f) ≫
    [#:when (flonum? (syntax-e #'f))]
    --------
-   [⊢ [[_ ≫ (#%datum- . f)] ⇒ : Float]]]
+   [⊢ [_ ≫ (#%datum- . f) ⇒ : Float]]]
   [(#%datum . c:char) ≫
    --------
-   [⊢ [[_ ≫ (#%datum- . c)] ⇒ : Char]]]
+   [⊢ [_ ≫ (#%datum- . c) ⇒ : Char]]]
   [(#%datum . x) ≫
    --------
    [_ ≻ (stlc+lit:#%datum . x)]])
@@ -50,16 +50,16 @@
 
 (define-typed-syntax and
   [(and e1 e2) ≫
-   [⊢ [[e1 ≫ e1-] ⇐ : Bool]]
-   [⊢ [[e2 ≫ e2-] ⇐ : Bool]]
+   [⊢ [e1 ≫ e1- ⇐ : Bool]]
+   [⊢ [e2 ≫ e2- ⇐ : Bool]]
    --------
-   [⊢ [[_ ≫ (and- e1- e2-)] ⇒ : Bool]]])
+   [⊢ [_ ≫ (and- e1- e2-) ⇒ : Bool]]])
 
 (define-typed-syntax or
   [(or e ...) ≫
-   [⊢ [[e ≫ e-] ⇐ : Bool] ...]
+   [⊢ [e ≫ e- ⇐ : Bool] ...]
    --------
-   [⊢ [[_ ≫ (or- e- ...)] ⇒ : Bool]]])
+   [⊢ [_ ≫ (or- e- ...) ⇒ : Bool]]])
 
 (begin-for-syntax 
   (define current-join 
@@ -80,44 +80,44 @@
 
 (define-typed-syntax if
   [(if e_tst e1 e2) ⇐ : τ-expected ≫
-   [⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
-   [⊢ [[e1 ≫ e1-] ⇐ : τ-expected]]
-   [⊢ [[e2 ≫ e2-] ⇐ : τ-expected]]
+   [⊢ [e_tst ≫ e_tst- ⇒ : _]] ; Any non-false value is truthy.
+   [⊢ [e1 ≫ e1- ⇐ : τ-expected]]
+   [⊢ [e2 ≫ e2- ⇐ : τ-expected]]
    --------
-   [⊢ [[_ ≫ (if- e_tst- e1- e2-)] ⇐ : _]]]
+   [⊢ [_ ≫ (if- e_tst- e1- e2-) ⇐ : _]]]
   [(if e_tst e1 e2) ≫
-   [⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
-   [⊢ [[e1 ≫ e1-] ⇒ : τ1]]
-   [⊢ [[e2 ≫ e2-] ⇒ : τ2]]
+   [⊢ [e_tst ≫ e_tst- ⇒ : _]] ; Any non-false value is truthy.
+   [⊢ [e1 ≫ e1- ⇒ : τ1]]
+   [⊢ [e2 ≫ e2- ⇒ : τ2]]
    --------
-   [⊢ [[_ ≫ (if- e_tst- e1- e2-)] ⇒ : (⊔ τ1 τ2)]]])
+   [⊢ [_ ≫ (if- e_tst- e1- e2-) ⇒ : (⊔ τ1 τ2)]]])
 
 (define-base-type Unit)
 (define-primop void : (→ Unit))
 
 (define-typed-syntax begin
   [(begin e_unit ... e) ⇐ : τ_expected ≫
-   [⊢ [[e_unit ≫ e_unit-] ⇒ : _] ...]
-   [⊢ [[e ≫ e-] ⇐ : τ_expected]]
+   [⊢ [e_unit ≫ e_unit- ⇒ : _] ...]
+   [⊢ [e ≫ e- ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (begin- e_unit- ... e-)] ⇐ : _]]]
+   [⊢ [_ ≫ (begin- e_unit- ... e-) ⇐ : _]]]
   [(begin e_unit ... e) ≫
-   [⊢ [[e_unit ≫ e_unit-] ⇒ : _] ...]
-   [⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [⊢ [e_unit ≫ e_unit- ⇒ : _] ...]
+   [⊢ [e ≫ e- ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ (begin- e_unit- ... e-)] ⇒ : τ_e]]])
+   [⊢ [_ ≫ (begin- e_unit- ... e-) ⇒ : τ_e]]])
 
 (define-typed-syntax let
   [(let ([x e] ...) e_body) ⇐ : τ_expected ≫
-   [⊢ [[e ≫ e-] ⇒ : τ_x] ...]
-   [() ([x : τ_x ≫ x-] ...) ⊢ [[e_body ≫ e_body-] ⇐ : τ_expected]]
+   [⊢ [e ≫ e- ⇒ : τ_x] ...]
+   [() ([x ≫ x- : τ_x] ...) ⊢ [e_body ≫ e_body- ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (let- ([x- e-] ...) e_body-)] ⇐ : _]]]
+   [⊢ [_ ≫ (let- ([x- e-] ...) e_body-) ⇐ : _]]]
   [(let ([x e] ...) e_body) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ_x] ...]
-   [() ([x : τ_x ≫ x-] ...) ⊢ [[e_body ≫ e_body-] ⇒ : τ_body]]
+   [⊢ [e ≫ e- ⇒ : τ_x] ...]
+   [() ([x ≫ x- : τ_x] ...) ⊢ [e_body ≫ e_body- ⇒ : τ_body]]
    --------
-   [⊢ [[_ ≫ (let- ([x- e-] ...) e_body-)] ⇒ : τ_body]]])
+   [⊢ [_ ≫ (let- ([x- e-] ...) e_body-) ⇒ : τ_body]]])
 
 ; dont need to manually transfer expected type
 ; result template automatically propagates properties
@@ -133,14 +133,14 @@
 
 (define-typed-syntax letrec
   [(letrec ([b:type-bind e] ...) e_body) ⇐ : τ_expected ≫
-   [() ([b.x : b.type ≫ x-] ...)
-    ⊢ [[e ≫ e-] ⇐ : b.type] ... [[e_body ≫ e_body-] ⇐ : τ_expected]]
+   [() ([b.x ≫ x- : b.type] ...)
+    ⊢ [e ≫ e- ⇐ : b.type] ... [e_body ≫ e_body- ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (letrec- ([x- e-] ...) e_body-)] ⇐ : _]]]
+   [⊢ [_ ≫ (letrec- ([x- e-] ...) e_body-) ⇐ : _]]]
   [(letrec ([b:type-bind e] ...) e_body) ≫
-   [() ([b.x : b.type ≫ x-] ...)
-    ⊢ [[e ≫ e-] ⇐ : b.type] ... [[e_body ≫ e_body-] ⇒ : τ_body]]
+   [() ([b.x ≫ x- : b.type] ...)
+    ⊢ [e ≫ e- ⇐ : b.type] ... [e_body ≫ e_body- ⇒ : τ_body]]
    --------
-   [⊢ [[_ ≫ (letrec- ([x- e-] ...) e_body-)] ⇒ : τ_body]]])
+   [⊢ [_ ≫ (letrec- ([x- e-] ...) e_body-) ⇒ : τ_body]]])
 
 
diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt
index 9e313c0..eaa5933 100644
--- a/turnstile/examples/fomega.rkt
+++ b/turnstile/examples/fomega.rkt
@@ -84,33 +84,33 @@
 
 (define-typed-syntax Λ
   [(Λ bvs:kind-ctx e) ≫
-   [([bvs.x : bvs.kind ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ [e ≫ e- ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
+   [⊢ [_ ≫ e- ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
 
 (define-typed-syntax inst
   [(inst e τ ...) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
-   [⊢ [[τ ≫ τ-] ⇐ : k] ...]
+   [⊢ [e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
+   [⊢ [τ ≫ τ- ⇐ : k] ...]
    [#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : τ-inst]]])
+   [⊢ [_ ≫ e- ⇒ : τ-inst]]])
 
 ;; TODO: merge with regular λ and app?
 ;; - see fomega2.rkt
 (define-typed-syntax tyλ
   [(tyλ bvs:kind-ctx τ_body) ≫
-   [() ([bvs.x : bvs.kind ≫ tv-] ...) ⊢ [[τ_body ≫ τ_body-] ⇒ : k_body]]
+   [() ([bvs.x ≫ tv- : bvs.kind] ...) ⊢ [τ_body ≫ τ_body- ⇒ : k_body]]
    [#:fail-unless ((current-kind?) #'k_body)
     (format "not a valid type: ~a\n" (type->str #'τ_body))]
    --------
-   [⊢ [[_ ≫ (λ- (tv- ...) τ_body-)] ⇒ : (⇒ bvs.kind ... k_body)]]])
+   [⊢ [_ ≫ (λ- (tv- ...) τ_body-) ⇒ : (⇒ bvs.kind ... k_body)]]])
 
 (define-typed-syntax tyapp
   [(tyapp τ_fn τ_arg ...) ≫
-   [⊢ [[τ_fn ≫ τ_fn-] ⇒ : (~⇒ k_in ... k_out)]]
+   [⊢ [τ_fn ≫ τ_fn- ⇒ : (~⇒ k_in ... k_out)]]
    [#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
     (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])]
-   [⊢ [[τ_arg ≫ τ_arg-] ⇐ : k_in] ...]
+   [⊢ [τ_arg ≫ τ_arg- ⇐ : k_in] ...]
    --------
-   [⊢ [[_ ≫ (#%app- τ_fn- τ_arg- ...)] ⇒ : k_out]]])
+   [⊢ [_ ≫ (#%app- τ_fn- τ_arg- ...) ⇒ : k_out]]])
diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt
index c953b86..b3ec142 100644
--- a/turnstile/examples/fomega2.rkt
+++ b/turnstile/examples/fomega2.rkt
@@ -80,15 +80,15 @@
 
 (define-typed-syntax Λ
   [(Λ bvs:kind-ctx e) ≫
-   [() ([bvs.x : bvs.kind ≫ tv-] ...) ⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [() ([bvs.x ≫ tv- : bvs.kind] ...) ⊢ [e ≫ e- ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
+   [⊢ [_ ≫ e- ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
 
 (define-typed-syntax inst
   [(inst e τ ...) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
-   [⊢ [[τ ≫ τ-] ⇐ : k] ...]
+   [⊢ [e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
+   [⊢ [τ ≫ τ- ⇐ : k] ...]
    [#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : τ-inst]]])
+   [⊢ [_ ≫ e- ⇒ : τ-inst]]])
 
diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt
index 74e3f26..adf43bb 100644
--- a/turnstile/examples/fsub.rkt
+++ b/turnstile/examples/fsub.rkt
@@ -48,7 +48,7 @@
   [(∀ ([tv:id <: τ:type] ...) τ_body) ≫
    --------
    ; eval first to overwrite the old #%type
-   [⊢ [[_ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body))] ⇒ : (<: τ.norm ...)]]])
+   [⊢ [_ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) ⇒ : (<: τ.norm ...)]]])
 (begin-for-syntax
   (define-syntax ~∀
     (pattern-expander
@@ -79,14 +79,14 @@
    ;; environment with a syntax property using another tag: '<:
    ;; The "expose" function looks for this tag to enforce the bound,
    ;; as in TaPL (fig 28-1)
-   [([tv : #%type <: τsub ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [([tv ≫ tv- : #%type <: τsub] ...) () ⊢ [e ≫ e- ⇒ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- <: τsub] ...) τ_e)]]])
+   [⊢ [_ ≫ e- ⇒ : (∀ ([tv- <: τsub] ...) τ_e)]]])
 (define-typed-syntax inst
   [(inst e τ:type ...) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~∀ ([tv <: τ_sub] ...) τ_body)]]
+   [⊢ [e ≫ e- ⇒ : (~∀ ([tv <: τ_sub] ...) τ_body)]]
    [τ.norm τ⊑ τ_sub #:for τ] ...
    [#:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : τ_inst]]])
+   [⊢ [_ ≫ e- ⇒ : τ_inst]]])
 
diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt
index ee408a4..1c3113a 100644
--- a/turnstile/examples/infer.rkt
+++ b/turnstile/examples/infer.rkt
@@ -148,24 +148,24 @@
    [#:with [X ...]
     (for/list ([X (in-list (generate-temporaries #'[x ...]))])
       (add-orig X X))]
-   [([X : #%type ≫ X-] ...) ([x : X ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇒ : τ_body*]]
+   [([X ≫ X- : #%type] ...) ([x ≫ x- : X] ...)
+    ⊢ [body ≫ body- ⇒ : τ_body*]]
    [#:with (~?Some [V ...] τ_body (~Cs [id_2 τ_2] ...)) (syntax-local-introduce #'τ_body*)]
    [#:with τ_fn (some/inst/generalize #'[X- ... V ...]
                                       #'(→ X- ... τ_body)
                                       #'([id_2 τ_2] ...))]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇒ : τ_fn]]])
+   [⊢ [_ ≫ (λ- (x- ...) body-) ⇒ : τ_fn]]])
 
 (define-typed-syntax #%app
   [(_ e_fn e_arg ...) ≫
    [#:with [A ...] (generate-temporaries #'[e_arg ...])]
    [#:with B (generate-temporary 'result)]
-   [⊢ [[e_fn ≫ e_fn-] ⇒ : τ_fn*]]
+   [⊢ [e_fn ≫ e_fn- ⇒ : τ_fn*]]
    [#:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_3 τ_4] ...))
     (syntax-local-introduce #'τ_fn*)]
    [#:with τ_fn-expected (tycons #'→ #'[A ... B])]
-   [⊢ [[e_arg ≫ e_arg-] ⇒ : τ_arg*] ...]
+   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg*] ...]
    [#:with [(~?Some [V3 ...] (~?∀ (V4 ...) τ_arg) (~Cs [τ_5 τ_6] ...)) ...]
     (syntax-local-introduce #'[τ_arg* ...])]
    [#:with τ_out (some/inst/generalize #'[A ... B V1 ... V2 ... V3 ... ... V4 ... ...]
@@ -175,11 +175,11 @@
                                           [A τ_arg] ...
                                           [τ_5 τ_6] ... ...))]
    --------
-   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out]]])
+   [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
 
 (define-typed-syntax ann #:datum-literals (:)
   [(ann e:expr : τ:type) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [⊢ [e ≫ e- ⇒ : τ_e]]
    [#:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_1 τ_2] ...))
     (syntax-local-introduce #'τ_e)]
    [#:with τ_e* (some/inst/generalize #'[V1 ... V2 ...]
@@ -189,11 +189,11 @@
                                          ...))]
    [τ_e* τ⊑ τ.norm #:for e]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : τ.norm]]])
+   [⊢ [_ ≫ e- ⇒ : τ.norm]]])
 
 (define-typed-syntax define
   [(define x:id e:expr) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [⊢ [e ≫ e- ⇒ : τ_e]]
    [#:with tmp (generate-temporary #'x)]
    --------
    [_ ≻ (begin-
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
index 1a46f53..ab7ce32 100644
--- a/turnstile/examples/mlish.rkt
+++ b/turnstile/examples/mlish.rkt
@@ -312,7 +312,7 @@
 ;;   intuitive, we arbitrarily sort the inferred tyvars lexicographically
 (define-typed-syntax define
   [(define x:id e) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ]]
+   [⊢ [e ≫ e- ⇒ : τ]]
    [#:with y (generate-temporary)]
    --------
    [_ ≻ (begin-
@@ -469,12 +469,12 @@
              [C:id ⇐ : (NameExpander τ-expected-arg (... ...)) ≫
               [#:when (stx-null? #'(τ ...))]
               --------
-              [⊢ [[_ ≫ (StructName)] ⇐ : _]]]
+              [⊢ [_ ≫ (StructName) ⇐ : _]]]
              ; id with multiple expected args, HO fn
              [C:id ≫
               [#:when (not (stx-null? #'(τ ...)))]
               --------
-              [⊢ [[_ ≫ StructName] ⇒ : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]]
+              [⊢ [_ ≫ StructName ⇒ : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]]
              [(C τs e_arg ...) ≫
               [#:when (brace? #'τs)] ; commit to this clause
               [#:with [X* (... ...)] #'[X ...]]
@@ -482,10 +482,10 @@
               [#:with {~! τ_X:type (... ...)} #'τs]
               [#:with (τ_in:type (... ...)) ; instantiated types
                (inst-types/cs #'(X ...) #'([X* τ_X.norm] (... ...)) #'(τ ...))]
-              [⊢ [[e_arg* ≫ e_arg*-] ⇐ : τ_in.norm] (... ...)]
+              [⊢ [e_arg* ≫ e_arg*- ⇐ : τ_in.norm] (... ...)]
               [#:with [e_arg- ...] #'[e_arg*- (... ...)]]
               --------
-              [⊢ [[_ ≫ (StructName e_arg- ...)] ⇒ : (Name τ_X.norm (... ...))]]]
+              [⊢ [_ ≫ (StructName e_arg- ...) ⇒ : (Name τ_X.norm (... ...))]]]
              [(C . args) ≫ ; no type annotations, must infer instantiation
               [#:with StructName/ty 
                (set-stx-prop/preserved
@@ -679,45 +679,45 @@
 (define-typed-syntax match2 #:datum-literals (with ->)
   [(match2 e with . clauses) ≫
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [⊢ [e ≫ e- ⇒ : τ_e]]
    [#:with ([(~seq p ...) -> e_body] ...) #'clauses]
    [#:with (pat ...) (stx-map ; use brace to indicate root pattern
                       (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
                       #'((p ...) ...)) ]
    [#:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)]
    [#:with ty-expected (get-expected-type stx)]
-   [() ([x : ty ≫ x-] ...)
-    ⊢ [[(add-expected e_body ty-expected) ≫ e_body-] ⇒ : ty_body]]
+   [() ([x ≫ x- : ty] ...)
+    ⊢ [(add-expected e_body ty-expected) ≫ e_body- ⇒ : ty_body]]
    ...
    [#:when (check-exhaust #'(pat- ...) #'τ_e)]
    --------
-   [⊢ [[_ ≫ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...)]
+   [⊢ [_ ≫ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...)
        ⇒ : (⊔ ty_body ...)]]])
 
 (define-typed-syntax match #:datum-literals (with -> ::)
   ;; e is a tuple
   [(match e with . clauses) ≫
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [⊢ [e ≫ e- ⇒ : τ_e]]
    [#:when (×? #'τ_e)]
    [#:with t_expect (get-expected-type stx)] ; propagate inferred type
    [#:with ([x ... -> e_body]) #'clauses]
    [#:with (~× ty ...) #'τ_e]
    [#:fail-unless (stx-length=? #'(ty ...) #'(x ...))
                   "match clause pattern not compatible with given tuple"]
-   [() ([x : ty ≫ x-] ...)
-    ⊢ [[(add-expected e_body t_expect) ≫ e_body-] ⇒ : ty_body]]
+   [() ([x ≫ x- : ty] ...)
+    ⊢ [(add-expected e_body t_expect) ≫ e_body- ⇒ : ty_body]]
    [#:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
                        #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))]
    [#:with z (generate-temporary)]
    --------
-   [⊢ [[_ ≫ (let- ([z e-])
-              (let- ([x- (acc z)] ...) e_body-))]
+   [⊢ [_ ≫ (let- ([z e-])
+             (let- ([x- (acc z)] ...) e_body-))
        ⇒ : ty_body]]]
   ;; e is a list
   [(match e with . clauses) ≫
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [⊢ [e ≫ e- ⇒ : τ_e]]
    [#:when (List? #'τ_e)]
    [#:with t_expect (get-expected-type stx)] ; propagate inferred type
    [#:with ([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
@@ -732,8 +732,8 @@
                             (= 1 (stx-length #'(xs ...)))))
     "match: missing non-empty list case"]
    [#:with (~List ty) #'τ_e]
-   [() ([x : ty ≫ x-] ... [rst : (List ty) ≫ rst-])
-    ⊢ [[(add-expected e_body t_expect) ≫ e_body-] ⇒ : ty_body]]
+   [() ([x ≫ x- : ty] ... [rst ≫ rst- : (List ty)])
+    ⊢ [(add-expected e_body t_expect) ≫ e_body- ⇒ : ty_body]]
    ...
    [#:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))]
    [#:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...))]
@@ -747,15 +747,15 @@
                              #'((x ...) ...))]
    [#:with (acc2 ...) (stx-map (lambda (l) #`(lambda- (lst) (list-tail- lst #,l))) #'(len ...))]
    --------
-   [⊢ [[_ ≫ (let- ([z e-])
-              (cond-
-                [(pred? z)
-                 (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))]
+   [⊢ [_ ≫ (let- ([z e-])
+             (cond-
+               [(pred? z)
+                (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))
        ⇒ : (⊔ ty_body ...)]]]
   ;; e is a variant
   [(match e with . clauses) ≫
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [⊢ [e ≫ e- ⇒ : τ_e]]
    [#:when (and (not (×? #'τ_e)) (not (List? #'τ_e)))]
    [#:with t_expect (get-expected-type stx)] ; propagate inferred type
    [#:with ([Clause:id x:id ... 
@@ -791,16 +791,16 @@
    ;;                             #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
    ;;                          #'((acc-fn ...) ...))]
    [#:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))]
-   [() ([x : τ ≫ x-] ...)
-    ⊢ [[e_guard ≫ e_guard-] ⇐ : Bool] [[e_c ≫ e_c-] ⇒ : τ_ec]]
+   [() ([x ≫ x- : τ] ...)
+    ⊢ [e_guard ≫ e_guard- ⇐ : Bool] [e_c ≫ e_c- ⇒ : τ_ec]]
    ...
    [#:with z (generate-temporary)] ; dont duplicate eval of test expr
    --------
-   [⊢ [[_ ≫ (let- ([z e-])
-              (cond-
-                [(and- (Cons? z) 
-                       (let- ([x- (acc z)] ...) e_guard-))
-                 (let- ([x- (acc z)] ...) e_c-)] ...))]
+   [⊢ [_ ≫ (let- ([z e-])
+             (cond-
+               [(and- (Cons? z) 
+                      (let- ([x- (acc z)] ...) e_guard-))
+                (let- ([x- (acc z)] ...) e_c-)] ...))
        ⇒ : (⊔ τ_ec ...)]]])
 
 ; special arrow that computes free vars; for use with tests
@@ -840,37 +840,37 @@
    [#:fail-unless (stx-length=? #'[x ...] #'[τ_in ...])
     (format "expected a function of ~a arguments, got one with ~a arguments"
             (stx-length #'[τ_in ...]) (stx-length #'[x ...]))]
-   [([X : #%type ≫ X-] ...) ([x : τ_in ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇐ : τ_out]]
+   [([X ≫ X- : #%type] ...) ([x ≫ x- : τ_in] ...)
+    ⊢ [body ≫ body- ⇐ : τ_out]]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇐ : _]]]
+   [⊢ [_ ≫ (λ- (x- ...) body-) ⇐ : _]]]
   [(λ ([x : τ_x] ...) body) ⇐ : (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ≫
    [#:with [X ...] (compute-tyvars #'(τ_x ...))]
-   [([X : #%type ≫ X-] ...) ()
-    ⊢ [[τ_x ≫ τ_x-] ⇐ : #%type] ...]
+   [([X ≫ X- : #%type] ...) ()
+    ⊢ [τ_x ≫ τ_x- ⇐ : #%type] ...]
    [τ_in τ⊑ τ_x- #:for x] ...
    ;; TODO is there a way to have λs that refer to ids defined after them?
-   [([V : #%type ≫ V-] ... [X- : #%type ≫ X--] ...) ([x : τ_x- ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇐ : τ_out]]
+   [([V ≫ V- : #%type] ... [X- ≫ X-- : #%type] ...) ([x ≫ x- : τ_x-] ...)
+    ⊢ [body ≫ body- ⇐ : τ_out]]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇐ : _]]]
+   [⊢ [_ ≫ (λ- (x- ...) body-) ⇐ : _]]]
   [(λ ([x : τ_x] ...) body) ≫
    [#:with [X ...] (compute-tyvars #'(τ_x ...))]
    ;; TODO is there a way to have λs that refer to ids defined after them?
-   [([X : #%type ≫ X-] ...) ([x : τ_x ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇒ : τ_body]]
+   [([X ≫ X- : #%type] ...) ([x ≫ x- : τ_x] ...)
+    ⊢ [body ≫ body- ⇒ : τ_body]]
    [#:with [τ_x* ...] (inst-types/cs #'[X ...] #'([X X-] ...) #'[τ_x ...])]
    [#:with τ_fn (add-orig #'(?∀ (X- ...) (ext-stlc:→ τ_x* ... τ_body))
                           #`(→ #,@(stx-map get-orig #'[τ_x* ...]) #,(get-orig #'τ_body)))]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇒ : τ_fn]]])
+   [⊢ [_ ≫ (λ- (x- ...) body-) ⇒ : τ_fn]]])
 
 
 ;; #%app --------------------------------------------------
 (define-typed-syntax mlish:#%app #:export-as #%app
   [(_ e_fn e_arg ...) ≫
    ;; compute fn type (ie ∀ and →)
-   [⊢ [[e_fn ≫ e_fn-] ⇒ : (~?∀ Xs (~ext-stlc:→ . tyX_args))]]
+   [⊢ [e_fn ≫ e_fn- ⇒ : (~?∀ Xs (~ext-stlc:→ . tyX_args))]]
    ;; solve for type variables Xs
    [#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args stx)]
    ;; instantiate polymorphic function type
@@ -897,7 +897,7 @@
                               stx)))
                          #'(∀ (unsolved-X ... Y ...) τ_out)]))]
    --------
-   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out*]]])
+   [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out*]]])
 
 
 ;; cond and other conditionals
@@ -906,29 +906,29 @@
                test)
           b ... body] ...+)
    ⇐ : τ_expected ≫
-   [⊢ [[test ≫ test-] ⇐ : Bool] ...]
-   [⊢ [[(begin b ... body) ≫ body-] ⇐ : τ_expected] ...]
+   [⊢ [test ≫ test- ⇐ : Bool] ...]
+   [⊢ [(begin b ... body) ≫ body- ⇐ : τ_expected] ...]
    --------
-   [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇐ : _]]]
+   [⊢ [_ ≫ (cond- [test- body-] ...) ⇐ : _]]]
   [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
                test)
           b ... body] ...+) ≫
-   [⊢ [[test ≫ test-] ⇐ : Bool] ...]
-   [⊢ [[(begin b ... body) ≫ body-] ⇒ : τ_body] ...]
+   [⊢ [test ≫ test- ⇐ : Bool] ...]
+   [⊢ [(begin b ... body) ≫ body- ⇒ : τ_body] ...]
    --------
-   [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇒ : (⊔ τ_body ...)]]])
+   [⊢ [_ ≫ (cond- [test- body-] ...) ⇒ : (⊔ τ_body ...)]]])
 (define-typed-syntax when
   [(when test body ...) ≫
-   [⊢ [[test ≫ test-] ⇒ : _]]
-   [⊢ [[body ≫ body-] ⇒ : _] ...]
+   [⊢ [test ≫ test- ⇒ : _]]
+   [⊢ [body ≫ body- ⇒ : _] ...]
    --------
-   [⊢ [[_ ≫ (when- test- body- ... (void-))] ⇒ : Unit]]])
+   [⊢ [_ ≫ (when- test- body- ... (void-)) ⇒ : Unit]]])
 (define-typed-syntax unless
   [(unless test body ...) ≫
-   [⊢ [[test ≫ test-] ⇒ : _]]
-   [⊢ [[body ≫ body-] ⇒ : _] ...]
+   [⊢ [test ≫ test- ⇒ : _]]
+   [⊢ [body ≫ body- ⇒ : _] ...]
    --------
-   [⊢ [[_ ≫ (unless- test- body- ... (void-))] ⇒ : Unit]]])
+   [⊢ [_ ≫ (unless- test- body- ... (void-)) ⇒ : Unit]]])
 
 ;; sync channels and threads
 (define-type-constructor Channel)
@@ -937,31 +937,31 @@
   [(make-channel (~and tys {ty})) ≫
    [#:when (brace? #'tys)]
    --------
-   [⊢ [[_ ≫ (make-channel-)] ⇒ : (Channel ty)]]])
+   [⊢ [_ ≫ (make-channel-) ⇒ : (Channel ty)]]])
 (define-typed-syntax channel-get
   [(channel-get c) ⇐ : ty ≫
-   [⊢ [[c ≫ c-] ⇐ : (Channel ty)]]
+   [⊢ [c ≫ c- ⇐ : (Channel ty)]]
    --------
-   [⊢ [[_ ≫ (channel-get- c-)] ⇐ : _]]]
+   [⊢ [_ ≫ (channel-get- c-) ⇐ : _]]]
   [(channel-get c) ≫
-   [⊢ [[c ≫ c-] ⇒ : (~Channel ty)]]
+   [⊢ [c ≫ c- ⇒ : (~Channel ty)]]
    --------
-   [⊢ [[_ ≫ (channel-get- c-)] ⇒ : ty]]])
+   [⊢ [_ ≫ (channel-get- c-) ⇒ : ty]]])
 (define-typed-syntax channel-put
   [(channel-put c v) ≫
-   [⊢ [[c ≫ c-] ⇒ : (~Channel ty)]]
-   [⊢ [[v ≫ v-] ⇐ : ty]]
+   [⊢ [c ≫ c- ⇒ : (~Channel ty)]]
+   [⊢ [v ≫ v- ⇐ : ty]]
    --------
-   [⊢ [[_ ≫ (channel-put- c- v-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (channel-put- c- v-) ⇒ : Unit]]])
 
 (define-base-type Thread)
 
 ;; threads
 (define-typed-syntax thread
   [(thread th) ≫
-   [⊢ [[th ≫ th-] ⇒ : (~?∀ () (~ext-stlc:→ τ_out))]]
+   [⊢ [th ≫ th- ⇒ : (~?∀ () (~ext-stlc:→ τ_out))]]
    --------
-   [⊢ [[_ ≫ (thread- th-)] ⇒ : Thread]]])
+   [⊢ [_ ≫ (thread- th-) ⇒ : Thread]]])
 
 (define-primop random : (→ Int Int))
 (define-primop integer->char : (→ Int Char))
@@ -971,15 +971,15 @@
 (define-typed-syntax number->string
   [number->string:id ≫
    --------
-   [⊢ [[_ ≫ number->string-] ⇒ : (→ Int String)]]]
+   [⊢ [_ ≫ number->string- ⇒ : (→ Int String)]]]
   [(number->string n) ≫
    --------
    [_ ≻ (number->string n (ext-stlc:#%datum . 10))]]
   [(number->string n rad) ≫
-   [⊢ [[n ≫ n-] ⇐ : Int]]
-   [⊢ [[rad ≫ rad-] ⇐ : Int]]
+   [⊢ [n ≫ n- ⇐ : Int]]
+   [⊢ [rad ≫ rad- ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (number->string- n rad)] ⇒ : String]]])
+   [⊢ [_ ≫ (number->string- n rad) ⇒ : String]]])
 (define-primop string : (→ Char String))
 (define-primop sleep : (→ Int Unit))
 (define-primop string=? : (→ String String Bool))
@@ -987,9 +987,9 @@
 
 (define-typed-syntax string-append
   [(string-append str ...) ≫
-   [⊢ [[str ≫ str-] ⇐ : String] ...]
+   [⊢ [str ≫ str- ⇐ : String] ...]
    --------
-   [⊢ [[_ ≫ (string-append- str- ...)] ⇒ : String]]])
+   [⊢ [_ ≫ (string-append- str- ...) ⇒ : String]]])
 
 ;; vectors
 (define-type-constructor Vector)
@@ -998,56 +998,56 @@
   [(vector (~and tys {ty})) ≫
    [#:when (brace? #'tys)]
    --------
-   [⊢ [[_ ≫ (vector-)] ⇒ : (Vector ty)]]]
+   [⊢ [_ ≫ (vector-) ⇒ : (Vector ty)]]]
   [(vector v ...) ⇐ : (Vector ty) ≫
-   [⊢ [[v ≫ v-] ⇐ : ty] ...]
+   [⊢ [v ≫ v- ⇐ : ty] ...]
    --------
-   [⊢ [[_ ≫ (vector- v- ...)] ⇐ : _]]]
+   [⊢ [_ ≫ (vector- v- ...) ⇐ : _]]]
   [(vector v ...) ≫
-   [⊢ [[v ≫ v-] ⇒ : ty] ...]
+   [⊢ [v ≫ v- ⇒ : ty] ...]
    [#:when (same-types? #'(ty ...))]
    [#:with one-ty (stx-car #'(ty ...))]
    --------
-   [⊢ [[_ ≫ (vector- v- ...)] ⇒ : (Vector one-ty)]]])
+   [⊢ [_ ≫ (vector- v- ...) ⇒ : (Vector one-ty)]]])
 (define-typed-syntax make-vector
   [(make-vector n) ≫
    --------
    [_ ≻ (make-vector n (ext-stlc:#%datum . 0))]]
   [(make-vector n e) ≫
-   [⊢ [[n ≫ n-] ⇐ : Int]]
-   [⊢ [[e ≫ e-] ⇒ : ty]]
+   [⊢ [n ≫ n- ⇐ : Int]]
+   [⊢ [e ≫ e- ⇒ : ty]]
    --------
-   [⊢ [[_ ≫ (make-vector- n- e-)] ⇒ : (Vector ty)]]])
+   [⊢ [_ ≫ (make-vector- n- e-) ⇒ : (Vector ty)]]])
 (define-typed-syntax vector-length
   [(vector-length e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Vector _)]]
+   [⊢ [e ≫ e- ⇒ : (~Vector _)]]
    --------
-   [⊢ [[_ ≫ (vector-length- e-)] ⇒ : Int]]])
+   [⊢ [_ ≫ (vector-length- e-) ⇒ : Int]]])
 (define-typed-syntax vector-ref
   [(vector-ref e n) ⇐ : ty ≫
-   [⊢ [[e ≫ e-] ⇐ : (Vector ty)]]
-   [⊢ [[n ≫ n-] ⇐ : Int]]
+   [⊢ [e ≫ e- ⇐ : (Vector ty)]]
+   [⊢ [n ≫ n- ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (vector-ref- e- n-)] ⇐ : _]]]
+   [⊢ [_ ≫ (vector-ref- e- n-) ⇐ : _]]]
   [(vector-ref e n) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
-   [⊢ [[n ≫ n-] ⇐ : Int]]
+   [⊢ [e ≫ e- ⇒ : (~Vector ty)]]
+   [⊢ [n ≫ n- ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (vector-ref- e- n-)] ⇒ : ty]]])
+   [⊢ [_ ≫ (vector-ref- e- n-) ⇒ : ty]]])
 (define-typed-syntax vector-set!
   [(vector-set! e n v) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
-   [⊢ [[n ≫ n-] ⇐ : Int]]
-   [⊢ [[v ≫ v-] ⇐ : ty]]
+   [⊢ [e ≫ e- ⇒ : (~Vector ty)]]
+   [⊢ [n ≫ n- ⇐ : Int]]
+   [⊢ [v ≫ v- ⇐ : ty]]
    --------
-   [⊢ [[_ ≫ (vector-set!- e- n- v-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (vector-set!- e- n- v-) ⇒ : Unit]]])
 (define-typed-syntax vector-copy!
   [(vector-copy! dest start src) ≫
-   [⊢ [[dest ≫ dest-] ⇒ : (~Vector ty)]]
-   [⊢ [[start ≫ start-] ⇐ : Int]]
-   [⊢ [[src ≫ src-] ⇐ : (Vector ty)]]
+   [⊢ [dest ≫ dest- ⇒ : (~Vector ty)]]
+   [⊢ [start ≫ start- ⇐ : Int]]
+   [⊢ [src ≫ src- ⇐ : (Vector ty)]]
    --------
-   [⊢ [[_ ≫ (vector-copy!- dest- start- src-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (vector-copy!- dest- start- src-) ⇒ : Unit]]])
 
 
 ;; sequences and for loops
@@ -1062,158 +1062,158 @@
    --------
    [_ ≻ (in-range start end (ext-stlc:#%datum . 1))]]
   [(in-range start end step) ≫
-   [⊢ [[start ≫ start-] ⇐ : Int]]
-   [⊢ [[end ≫ end-] ⇐ : Int]]
-   [⊢ [[step ≫ step-] ⇐ : Int]]
+   [⊢ [start ≫ start- ⇐ : Int]]
+   [⊢ [end ≫ end- ⇐ : Int]]
+   [⊢ [step ≫ step- ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (in-range- start- end- step-)] ⇒ : (Sequence Int)]]])
+   [⊢ [_ ≫ (in-range- start- end- step-) ⇒ : (Sequence Int)]]])
 
 (define-typed-syntax in-naturals
  [(in-naturals) ≫
   --------
   [_ ≻ (in-naturals (ext-stlc:#%datum . 0))]]
  [(in-naturals start) ≫
-  [⊢ [[start ≫ start-] ⇐ : Int]]
+  [⊢ [start ≫ start- ⇐ : Int]]
   --------
-  [⊢ [[_ ≫ (in-naturals- start-)] ⇒ : (Sequence Int)]]])
+  [⊢ [_ ≫ (in-naturals- start-) ⇒ : (Sequence Int)]]])
 
 
 (define-typed-syntax in-vector
   [(in-vector e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
+   [⊢ [e ≫ e- ⇒ : (~Vector ty)]]
    --------
-   [⊢ [[_ ≫ (in-vector- e-)] ⇒ : (Sequence ty)]]])
+   [⊢ [_ ≫ (in-vector- e-) ⇒ : (Sequence ty)]]])
 
 (define-typed-syntax in-list
   [(in-list e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~List ty)]]
+   [⊢ [e ≫ e- ⇒ : (~List ty)]]
    --------
-   [⊢ [[_ ≫ (in-list- e-)] ⇒ : (Sequence ty)]]])
+   [⊢ [_ ≫ (in-list- e-) ⇒ : (Sequence ty)]]])
 
 (define-typed-syntax in-lines
   [(in-lines e) ≫
-   [⊢ [[e ≫ e-] ⇐ : String]]
+   [⊢ [e ≫ e- ⇐ : String]]
    --------
-   [⊢ [[_ ≫ (in-lines- (open-input-string- e-))] ⇒ : (Sequence String)]]])
+   [⊢ [_ ≫ (in-lines- (open-input-string- e-)) ⇒ : (Sequence String)]]])
 
 (define-typed-syntax for
   [(for ([x:id e]...) b ... body) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([x : ty ≫ x-] ...)
-    ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇒ : _]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([x ≫ x- : ty] ...)
+    ⊢ [b ≫ b- ⇒ : _] ... [body ≫ body- ⇒ : _]]
    --------
-   [⊢ [[_ ≫ (for- ([x- e-] ...) b- ... body-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (for- ([x- e-] ...) b- ... body-) ⇒ : Unit]]])
 (define-typed-syntax for*
   [(for* ([x:id e]...) b ... body) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([x : ty ≫ x-] ...)
-    ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇒ : _]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([x ≫ x- : ty] ...)
+    ⊢ [b ≫ b- ⇒ : _] ... [body ≫ body- ⇒ : _]]
    --------
-   [⊢ [[_ ≫ (for*- ([x- e-] ...) b- ... body-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (for*- ([x- e-] ...) b- ... body-) ⇒ : Unit]]])
 
 (define-typed-syntax for/list
   [(for/list ([x:id e]...) body) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([x ≫ x- : ty] ...) ⊢ [body ≫ body- ⇒ : ty_body]]
    --------
-   [⊢ [[_ ≫ (for/list- ([x- e-] ...) body-)] ⇒ : (List ty_body)]]])
+   [⊢ [_ ≫ (for/list- ([x- e-] ...) body-) ⇒ : (List ty_body)]]])
 (define-typed-syntax for/vector
   [(for/vector ([x:id e]...) body) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([x ≫ x- : ty] ...) ⊢ [body ≫ body- ⇒ : ty_body]]
    --------
-   [⊢ [[_ ≫ (for/vector- ([x- e-] ...) body-)] ⇒ : (Vector ty_body)]]])
+   [⊢ [_ ≫ (for/vector- ([x- e-] ...) body-) ⇒ : (Vector ty_body)]]])
 (define-typed-syntax for*/vector
   [(for*/vector ([x:id e]...) body) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([x ≫ x- : ty] ...) ⊢ [body ≫ body- ⇒ : ty_body]]
    --------
-   [⊢ [[_ ≫ (for*/vector- ([x- e-] ...) body-)] ⇒ : (Vector ty_body)]]])
+   [⊢ [_ ≫ (for*/vector- ([x- e-] ...) body-) ⇒ : (Vector ty_body)]]])
 (define-typed-syntax for*/list
   [(for*/list ([x:id e]...) body) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([x ≫ x- : ty] ...) ⊢ [body ≫ body- ⇒ : ty_body]]
    --------
-   [⊢ [[_ ≫ (for*/list- ([x- e-] ...) body-)] ⇒ : (List ty_body)]]])
+   [⊢ [_ ≫ (for*/list- ([x- e-] ...) body-) ⇒ : (List ty_body)]]])
 (define-typed-syntax for/fold
   [(for/fold ([acc init]) ([x:id e] ...) body) ⇐ : τ_expected ≫
-   [⊢ [[init ≫ init-] ⇐ : τ_expected]]
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([acc : τ_expected ≫ acc-] [x : ty ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇐ : τ_expected]]
+   [⊢ [init ≫ init- ⇐ : τ_expected]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([acc ≫ acc- : τ_expected] [x ≫ x- : ty] ...)
+    ⊢ [body ≫ body- ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇐ : _]]]
+   [⊢ [_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-) ⇐ : _]]]
   [(for/fold ([acc init]) ([x:id e] ...) body) ≫
-   [⊢ [[init ≫ init-] ⇒ : τ_init]]
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([acc : τ_init ≫ acc-] [x : ty ≫ x-] ...)
-    ⊢ [[body ≫ body-] ⇐ : τ_init]]
+   [⊢ [init ≫ init- ⇒ : τ_init]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([acc ≫ acc- : τ_init] [x ≫ x- : ty] ...)
+    ⊢ [body ≫ body- ⇐ : τ_init]]
    --------
-   [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇒ : τ_init]]])
+   [⊢ [_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-) ⇒ : τ_init]]])
 
 (define-typed-syntax for/hash
   [(for/hash ([x:id e]...) body) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : (~× ty_k ty_v)]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([x ≫ x- : ty] ...) ⊢ [body ≫ body- ⇒ : (~× ty_k ty_v)]]
    --------
-   [⊢ [[_ ≫ (for/hash- ([x- e-] ...)
-              (let- ([t body-])
-                (values- (car- t) (cadr- t))))]
+   [⊢ [_ ≫ (for/hash- ([x- e-] ...)
+             (let- ([t body-])
+               (values- (car- t) (cadr- t))))
        ⇒ : (Hash ty_k ty_v)]]])
 
 (define-typed-syntax for/sum
   [(for/sum ([x:id e]... 
              (~optional (~seq #:when guard) #:defaults ([guard #'#t])))
      body) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
-   [() ([x : ty ≫ x-] ...)
-    ⊢ [[guard ≫ guard-] ⇒ : _] [[body ≫ body-] ⇐ : Int]]
+   [⊢ [e ≫ e- ⇒ : (~Sequence ty)] ...]
+   [() ([x ≫ x- : ty] ...)
+    ⊢ [guard ≫ guard- ⇒ : _] [body ≫ body- ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (for/sum- ([x- e-] ... #:when guard-) body-)] ⇒ : Int]]])
+   [⊢ [_ ≫ (for/sum- ([x- e-] ... #:when guard-) body-) ⇒ : Int]]])
 
 ; printing and displaying
 (define-typed-syntax printf
   [(printf str e ...) ≫
-   [⊢ [[str ≫ s-] ⇐ : String]]
-   [⊢ [[e ≫ e-] ⇒ : ty] ...]
+   [⊢ [str ≫ s- ⇐ : String]]
+   [⊢ [e ≫ e- ⇒ : ty] ...]
    --------
-   [⊢ [[_ ≫ (printf- s- e- ...)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (printf- s- e- ...) ⇒ : Unit]]])
 (define-typed-syntax format
   [(format str e ...) ≫
-   [⊢ [[str ≫ s-] ⇐ : String]]
-   [⊢ [[e ≫ e-] ⇒ : ty] ...]
+   [⊢ [str ≫ s- ⇐ : String]]
+   [⊢ [e ≫ e- ⇒ : ty] ...]
    --------
-   [⊢ [[_ ≫ (format- s- e- ...)] ⇒ : String]]])
+   [⊢ [_ ≫ (format- s- e- ...) ⇒ : String]]])
 (define-typed-syntax display
   [(display e) ≫
-   [⊢ [[e ≫ e-] ⇒ : _]]
+   [⊢ [e ≫ e- ⇒ : _]]
    --------
-   [⊢ [[_ ≫ (display- e-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (display- e-) ⇒ : Unit]]])
 (define-typed-syntax displayln
   [(displayln e) ≫
-   [⊢ [[e ≫ e-] ⇒ : _]]
+   [⊢ [e ≫ e- ⇒ : _]]
    --------
-   [⊢ [[_ ≫ (displayln- e-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (displayln- e-) ⇒ : Unit]]])
 (define-primop newline : (→ Unit))
 
 (define-typed-syntax list->vector
   [(list->vector e) ⇐ : (~Vector ty) ≫
-   [⊢ [[e ≫ e-] ⇐ : (List ty)]]
+   [⊢ [e ≫ e- ⇐ : (List ty)]]
    --------
-   [⊢ [[_ ≫ (list->vector- e-)] ⇐ : _]]]
+   [⊢ [_ ≫ (list->vector- e-) ⇐ : _]]]
   [(list->vector e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~List ty)]]
+   [⊢ [e ≫ e- ⇒ : (~List ty)]]
    --------
-   [⊢ [[_ ≫ (list->vector- e-)] ⇒ : (Vector ty)]]])
+   [⊢ [_ ≫ (list->vector- e-) ⇒ : (Vector ty)]]])
 
 (define-typed-syntax let
   [(let name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body) ≫
-   [⊢ [[e ≫ e-] ⇒ : ty_e] ...]
-   [() ([name : (→ ty_e ... ty.norm) ≫ name-] [x : ty_e ≫ x-] ...)
-    ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇐ : ty.norm]]
+   [⊢ [e ≫ e- ⇒ : ty_e] ...]
+   [() ([name ≫ name- : (→ ty_e ... ty.norm)] [x ≫ x- : ty_e] ...)
+    ⊢ [b ≫ b- ⇒ : _] ... [body ≫ body- ⇐ : ty.norm]]
    --------
-   [⊢ [[_ ≫ (letrec- ([name- (λ- (x- ...) b- ... body-)])
-              (name- e- ...))]
+   [⊢ [_ ≫ (letrec- ([name- (λ- (x- ...) b- ... body-)])
+             (name- e- ...))
        ⇒ : ty.norm]]]
   [(let ([x:id e] ...) body ...) ≫
    --------
@@ -1225,71 +1225,71 @@
 
 (define-typed-syntax begin
   [(begin body ... b) ⇐ : τ_expected ≫
-   [⊢ [[body ≫ body-] ⇒ : _] ...]
-   [⊢ [[b ≫ b-] ⇐ : τ_expected]]
+   [⊢ [body ≫ body- ⇒ : _] ...]
+   [⊢ [b ≫ b- ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (begin- body- ... b-)] ⇐ : _]]]
+   [⊢ [_ ≫ (begin- body- ... b-) ⇐ : _]]]
   [(begin body ... b) ≫
-   [⊢ [[body ≫ body-] ⇒ : _] ...]
-   [⊢ [[b ≫ b-] ⇒ : τ]]
+   [⊢ [body ≫ body- ⇒ : _] ...]
+   [⊢ [b ≫ b- ⇒ : τ]]
    --------
-   [⊢ [[_ ≫ (begin- body- ... b-)] ⇒ : τ]]])
+   [⊢ [_ ≫ (begin- body- ... b-) ⇒ : τ]]])
 
 ;; hash
 (define-type-constructor Hash #:arity = 2)
 
 (define-typed-syntax in-hash
   [(in-hash e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Hash ty_k ty_v)]]
+   [⊢ [e ≫ e- ⇒ : (~Hash ty_k ty_v)]]
    --------
-   [⊢ [[_ ≫ (hash-map- e- list-)] ⇒ : (Sequence (stlc+rec-iso:× ty_k ty_v))]]])
+   [⊢ [_ ≫ (hash-map- e- list-) ⇒ : (Sequence (stlc+rec-iso:× ty_k ty_v))]]])
 
 ; mutable hashes
 (define-typed-syntax hash
   [(hash (~and tys {ty_key ty_val})) ≫
    [#:when (brace? #'tys)]
    --------
-   [⊢ [[_ ≫ (make-hash-)] ⇒ : (Hash ty_key ty_val)]]]
+   [⊢ [_ ≫ (make-hash-) ⇒ : (Hash ty_key ty_val)]]]
   [(hash (~seq k v) ...) ≫
-   [⊢ [[k ≫ k-] ⇒ : ty_k] ...]
-   [⊢ [[v ≫ v-] ⇒ : ty_v] ...]
+   [⊢ [k ≫ k- ⇒ : ty_k] ...]
+   [⊢ [v ≫ v- ⇒ : ty_v] ...]
    [#:when (same-types? #'(ty_k ...))]
    [#:when (same-types? #'(ty_v ...))]
    [#:with ty_key (stx-car #'(ty_k ...))]
    [#:with ty_val (stx-car #'(ty_v ...))]
    --------
-   [⊢ [[_ ≫ (make-hash- (list- (cons- k- v-) ...))] ⇒ : (Hash ty_key ty_val)]]])
+   [⊢ [_ ≫ (make-hash- (list- (cons- k- v-) ...)) ⇒ : (Hash ty_key ty_val)]]])
 (define-typed-syntax hash-set!
   [(hash-set! h k v) ≫
-   [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
-   [⊢ [[k ≫ k-] ⇐ : ty_k]]
-   [⊢ [[v ≫ v-] ⇐ : ty_v]]
+   [⊢ [h ≫ h- ⇒ : (~Hash ty_k ty_v)]]
+   [⊢ [k ≫ k- ⇐ : ty_k]]
+   [⊢ [v ≫ v- ⇐ : ty_v]]
    --------
-   [⊢ [[_ ≫ (hash-set!- h- k- v-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (hash-set!- h- k- v-) ⇒ : Unit]]])
 (define-typed-syntax hash-ref
   [(hash-ref h k) ≫
-   [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
-   [⊢ [[k ≫ k-] ⇐ : ty_k]]
+   [⊢ [h ≫ h- ⇒ : (~Hash ty_k ty_v)]]
+   [⊢ [k ≫ k- ⇐ : ty_k]]
    --------
-   [⊢ [[_ ≫ (hash-ref- h- k-)] ⇒ : ty_v]]]
+   [⊢ [_ ≫ (hash-ref- h- k-) ⇒ : ty_v]]]
   [(hash-ref h k fail) ≫
-   [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
-   [⊢ [[k ≫ k-] ⇐ : ty_k]]
-   [⊢ [[fail ≫ fail-] ⇐ : (→ ty_v)]]
+   [⊢ [h ≫ h- ⇒ : (~Hash ty_k ty_v)]]
+   [⊢ [k ≫ k- ⇐ : ty_k]]
+   [⊢ [fail ≫ fail- ⇐ : (→ ty_v)]]
    --------
-   [⊢ [[_ ≫ (hash-ref- h- k- fail-)] ⇒ : ty_val]]])
+   [⊢ [_ ≫ (hash-ref- h- k- fail-) ⇒ : ty_val]]])
 (define-typed-syntax hash-has-key?
   [(hash-has-key? h k) ≫
-   [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k _)]]
-   [⊢ [[k ≫ k-] ⇐ : ty_k]]
+   [⊢ [h ≫ h- ⇒ : (~Hash ty_k _)]]
+   [⊢ [k ≫ k- ⇐ : ty_k]]
    --------
-   [⊢ [[_ ≫ (hash-has-key?- h- k-)] ⇒ : Bool]]])
+   [⊢ [_ ≫ (hash-has-key?- h- k-) ⇒ : Bool]]])
 
 (define-typed-syntax hash-count
   [(hash-count h) ≫
-   [⊢ [[h ≫ h-] ⇒ : (~Hash _ _)]]
+   [⊢ [h ≫ h- ⇒ : (~Hash _ _)]]
    --------
-   [⊢ [[_ ≫ (hash-count- h-)] ⇒ : Int]]])
+   [⊢ [_ ≫ (hash-count- h-) ⇒ : Int]]])
 
 (define-base-type String-Port)
 (define-base-type Input-Port)
@@ -1302,18 +1302,18 @@
   --------
   [_ ≻ (write-string str out (ext-stlc:#%datum . 0) (string-length str))]]
  [(write-string str out start end) ≫
-  [⊢ [[str ≫ str-] ⇐ : String]]
-  [⊢ [[out ≫ out-] ⇐ : String-Port]]
-  [⊢ [[start ≫ start-] ⇐ : Int]]
-  [⊢ [[end ≫ end-] ⇐ : Int]]
+  [⊢ [str ≫ str- ⇐ : String]]
+  [⊢ [out ≫ out- ⇐ : String-Port]]
+  [⊢ [start ≫ start- ⇐ : Int]]
+  [⊢ [end ≫ end- ⇐ : Int]]
   --------
-  [⊢ [[_ ≫ (begin- (write-string- str- out- start- end-) (void-))] ⇒ : Unit]]])
+  [⊢ [_ ≫ (begin- (write-string- str- out- start- end-) (void-)) ⇒ : Unit]]])
 
 (define-typed-syntax string-length
  [(string-length str) ≫
-  [⊢ [[str ≫ str-] ⇐ : String]]
+  [⊢ [str ≫ str- ⇐ : String]]
   --------
-  [⊢ [[_ ≫ (string-length- str-)] ⇒ : Int]]])
+  [⊢ [_ ≫ (string-length- str-) ⇒ : Int]]])
 (define-primop make-string : (→ Int String))
 (define-primop string-set! : (→ String Int Char Unit))
 (define-primop string-ref : (→ String Int Char))
@@ -1323,13 +1323,13 @@
    [_ ≻ (string-copy!
          dest dest-start src (ext-stlc:#%datum . 0) (string-length src))]]
   [(string-copy! dest dest-start src src-start src-end) ≫
-   [⊢ [[dest ≫ dest-] ⇐ : String]]
-   [⊢ [[src ≫ src-] ⇐ : String]]
-   [⊢ [[dest-start ≫ dest-start-] ⇐ : Int]]
-   [⊢ [[src-start ≫ src-start-] ⇐ : Int]]
-   [⊢ [[src-end ≫ src-end-] ⇐ : Int]]
+   [⊢ [dest ≫ dest- ⇐ : String]]
+   [⊢ [src ≫ src- ⇐ : String]]
+   [⊢ [dest-start ≫ dest-start- ⇐ : Int]]
+   [⊢ [src-start ≫ src-start- ⇐ : Int]]
+   [⊢ [src-end ≫ src-end- ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (string-copy!- dest- dest-start- src- src-start- src-end-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (string-copy!- dest- dest-start- src- src-start- src-end-) ⇒ : Unit]]])
 
 (define-primop fl+ : (→ Float Float Float))
 (define-primop fl- : (→ Float Float Float))
@@ -1344,20 +1344,20 @@
 (define-primop fx->fl : (→ Int Float))
 (define-typed-syntax quotient+remainder
   [(quotient+remainder x y) ≫
-   [⊢ [[x ≫ x-] ⇐ : Int]]
-   [⊢ [[y ≫ y-] ⇐ : Int]]
+   [⊢ [x ≫ x- ⇐ : Int]]
+   [⊢ [y ≫ y- ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (let-values- ([[a b] (quotient/remainder- x- y-)])
-              (list- a b))]
+   [⊢ [_ ≫ (let-values- ([[a b] (quotient/remainder- x- y-)])
+             (list- a b))
        ⇒ : (stlc+rec-iso:× Int Int)]]])
 (define-primop quotient : (→ Int Int Int))
 
 (define-typed-syntax set!
   [(set! x:id e) ≫
-   [⊢ [[x ≫ x-] ⇒ : ty_x]]
-   [⊢ [[e ≫ e-] ⇐ : ty_x]]
+   [⊢ [x ≫ x- ⇒ : ty_x]]
+   [⊢ [e ≫ e- ⇐ : ty_x]]
    --------
-   [⊢ [[_ ≫ (set!- x e-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (set!- x e-) ⇒ : Unit]]])
 
 (define-typed-syntax provide-type
   [(provide-type ty ...) ≫
@@ -1366,7 +1366,7 @@
 
 (define-typed-syntax provide
   [(provide x:id ...) ≫
-   [⊢ [[x ≫ x-] ⇒ : ty_x] ...]
+   [⊢ [x ≫ x- ⇒ : ty_x] ...]
    ; TODO: use hash-code to generate this tmp
    [#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))]
    --------
@@ -1389,17 +1389,17 @@
 
 (define-typed-syntax equal?
   [(equal? e1 e2) ≫
-   [⊢ [[e1 ≫ e1-] ⇒ : ty1]]
-   [⊢ [[e2 ≫ e2-] ⇐ : ty1]]
+   [⊢ [e1 ≫ e1- ⇒ : ty1]]
+   [⊢ [e2 ≫ e2- ⇐ : ty1]]
    --------
-   [⊢ [[_ ≫ (equal?- e1- e2-)] ⇒ : Bool]]])
+   [⊢ [_ ≫ (equal?- e1- e2-) ⇒ : Bool]]])
 
 (define-typed-syntax read-int
   [(read-int) ≫
    --------
-   [⊢ [[_ ≫ (let- ([x (read-)])
-              (cond- [(exact-integer?- x) x]
-                     [else (error- 'read-int "expected an int, given: ~v" x)]))]
+   [⊢ [_ ≫ (let- ([x (read-)])
+             (cond- [(exact-integer?- x) x]
+                    [else (error- 'read-int "expected an int, given: ~v" x)]))
        ⇒ : Int]]])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
index b67783b..04dc199 100644
--- a/turnstile/examples/rosette/bv.rkt
+++ b/turnstile/examples/rosette/bv.rkt
@@ -12,14 +12,14 @@
 (define-typed-syntax current-bvpred
   [c-bvpred:id ≫
    --------
-   [⊢ [[_ ≫ bv:BV] ⇒ : (Param BVPred)]]]
+   [⊢ [_ ≫ bv:BV ⇒ : (Param BVPred)]]]
   [(_) ≫
    --------
-   [⊢ [[_ ≫ (bv:BV)] ⇒ : BVPred]]]
+   [⊢ [_ ≫ (bv:BV) ⇒ : BVPred]]]
   [(_ e) ≫
-   [⊢ [[e ≫ e-] ⇒ : BVPred]]
+   [⊢ [e ≫ e- ⇒ : BVPred]]
    --------
-   [⊢ [[_ ≫ (bv:BV e-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (bv:BV e-) ⇒ : Unit]]])
 
 (define-typed-syntax bv
   [(_ e_val) ≫
@@ -34,9 +34,9 @@
    --------
    [_ ≻ (bv* (current-bvpred))]]
   [(_ e_size) ≫
-   [⊢ [[e_size ≫ e_size-] ⇐ : BVPred]]
+   [⊢ [e_size ≫ e_size- ⇐ : BVPred]]
    --------
-   [⊢ [[_ ≫ ((lambda- () (ro:define-symbolic* b e_size-) b))] ⇒ : BV]]])
+   [⊢ [_ ≫ ((lambda- () (ro:define-symbolic* b e_size-) b)) ⇒ : BV]]])
 
 (define-syntax-rule (bool->bv b) 
   (rosette:if b 
@@ -60,10 +60,10 @@
    --------
    [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv (rosette:#%datum . 4))]]
   [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫
-   [⊢ [[spec ≫ spec-] ⇒ : ty_spec]]
+   [⊢ [spec ≫ spec- ⇒ : ty_spec]]
    [#:fail-unless (→? #'ty_spec) "spec must be a function"]
-   [⊢ [[lib-expr ≫ lib-expr-] ⇐ : Lib]]
-   [⊢ [[minbv ≫ minbv-] ⇐ : Int]]
+   [⊢ [lib-expr ≫ lib-expr- ⇐ : Lib]]
+   [⊢ [minbv ≫ minbv- ⇐ : Int]]
    [#:with id-stx (format-id #'id "~a-stx" #'id #:source #'id)]
    --------
    [_ ≻ (begin-
@@ -80,14 +80,14 @@
   [(_ [(~and ids (id ...)) n] ...) ≫
    [#:fail-unless (stx-andmap brace? #'(ids ...))
                   "given ops must be enclosed with braces"]
-   [⊢ [[n ≫ n-] ⇐ : Int] ...]
-   [⊢ [[id ≫ id-] ⇒ : ty_id] ... ...]
+   [⊢ [n ≫ n- ⇐ : Int] ...]
+   [⊢ [id ≫ id- ⇒ : ty_id] ... ...]
    [#:fail-unless (stx-andmap →? #'(ty_id ... ...))
                   "given op must be a function"]
    [#:with ((~→ ty ...) ...) #'(ty_id ... ...)]
    [#:fail-unless (stx-andmap BV? #'(ty ... ...))
                   "given op must have BV inputs and output"]
    --------
-   [⊢ [[_ ≫ (bv:bvlib [{id- ...} n-] ...)] ⇒ : Lib]]])
+   [⊢ [_ ≫ (bv:bvlib [{id- ...} n-] ...) ⇒ : Lib]]])
 
 (define-syntax-rule (thunk e) (rosette:λ () e))
diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt
index dc6d08a..05fdcb4 100644
--- a/turnstile/examples/rosette/fsm.rkt
+++ b/turnstile/examples/rosette/fsm.rkt
@@ -16,9 +16,9 @@
 
 (define-typed-syntax pregexp 
   [(_ s) ≫
-   [⊢ [[s ≫ s-] ⇐ : String]]
+   [⊢ [s ≫ s- ⇐ : String]]
    --------
-   [⊢ [[_ ≫ (pregexp- s-)] ⇒ : Regexp]]])
+   [⊢ [_ ≫ (pregexp- s-) ⇒ : Regexp]]])
 
 (define-typed-syntax automaton #:datum-literals (: →)
   [(_ init-state:id
@@ -33,21 +33,21 @@
                       (member t states)))
                   (format "transition to unknown state")]
    [#:with arr (datum->syntax #f '→)]
-   [() ([state : State ≫ state-] ...) ⊢ 
-    [[init-state ≫ init-state-] ⇐ : State]
-    [[target ≫ target-] ⇐ : State] ... ...]
+   [() ([state ≫ state- : State] ...) ⊢ 
+    [init-state ≫ init-state- ⇐ : State]
+    [target ≫ target- ⇐ : State] ... ...]
    --------
-   [⊢ [[_ ≫ (fsm:automaton init-state- 
-              [state- : (label arr target-) ...] ...)] 
+   [⊢ [_ ≫ (fsm:automaton init-state-
+             [state- : (label arr target-) ...] ...)
        ⇒ : FSM]]])
 
 (define-primop reject : State)
 
 (define-typed-syntax ?
  [(_ e ...+) ≫
-   [⊢ [[e ≫ e-] ⇒ : ty]] ...
+   [⊢ [e ≫ e- ⇒ : ty]] ...
    --------
-   [⊢ [[_ ≫ (ro:choose e ...)] ⇒ : (⊔ ty ...)]]])
+   [⊢ [_ ≫ (ro:choose e ...) ⇒ : (⊔ ty ...)]]])
 
 (define (apply-FSM f v) (f v))
 (define-primop apply-FSM : (→ FSM (List Symbol) Bool))
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
index ae35c85..9403a78 100644
--- a/turnstile/examples/rosette/rosette.rkt
+++ b/turnstile/examples/rosette/rosette.rkt
@@ -20,7 +20,7 @@
 
 (define-typed-syntax define-symbolic
   [(_ x:id ...+ pred : ty:type) ≫
-   [⊢ [[pred ≫ pred-] ⇐ : (→ ty.norm Bool)]]
+   [⊢ [pred ≫ pred- ⇐ : (→ ty.norm Bool)]]
    [#:with (y ...) (generate-temporaries #'(x ...))]
    --------
    [_ ≻ (begin-
@@ -35,10 +35,10 @@
 (define-typed-syntax quote
   [(_ x:id) ≫
    --------
-   [⊢ [[_ ≫ (quote- x)] ⇒ : Symbol]]]
+   [⊢ [_ ≫ (quote- x) ⇒ : Symbol]]]
   [(_ (x:id ...)) ≫
    --------
-   [⊢ [[_ ≫ (quote- (x ...))] ⇒ : (stlc+cons:List Symbol)]]])
+   [⊢ [_ ≫ (quote- (x ...)) ⇒ : (stlc+cons:List Symbol)]]])
 
 (define-type-constructor Param #:arity = 1)
 
@@ -48,43 +48,43 @@
 
 (define-typed-syntax equal?
   [(equal? e1 e2) ≫
-   [⊢ [[e1 ≫ e1-] ⇒ : ty1]]
-   [⊢ [[e2 ≫ e2-] ⇐ : ty1]]
+   [⊢ [e1 ≫ e1- ⇒ : ty1]]
+   [⊢ [e2 ≫ e2- ⇐ : ty1]]
    --------
-   [⊢ [[_ ≫ (ro:equal? e1- e2-)] ⇒ : Bool]]])
+   [⊢ [_ ≫ (ro:equal? e1- e2-) ⇒ : Bool]]])
 
 (define-typed-syntax if
   [(if e_tst e1 e2) ⇐ : τ-expected ≫
-   [⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
-   [⊢ [[e1 ≫ e1-] ⇐ : τ-expected]]
-   [⊢ [[e2 ≫ e2-] ⇐ : τ-expected]]
+   [⊢ [e_tst ≫ e_tst- ⇒ : _]] ; Any non-false value is truthy.
+   [⊢ [e1 ≫ e1- ⇐ : τ-expected]]
+   [⊢ [e2 ≫ e2- ⇐ : τ-expected]]
    --------
-   [⊢ [[_ ≫ (ro:if e_tst- e1- e2-)] ⇐ : _]]]
+   [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇐ : _]]]
   [(if e_tst e1 e2) ≫
-   [⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
-   [⊢ [[e1 ≫ e1-] ⇒ : τ1]]
-   [⊢ [[e2 ≫ e2-] ⇒ : τ2]]
+   [⊢ [e_tst ≫ e_tst- ⇒ : _]] ; Any non-false value is truthy.
+   [⊢ [e1 ≫ e1- ⇒ : τ1]]
+   [⊢ [e2 ≫ e2- ⇒ : τ2]]
    --------
-   [⊢ [[_ ≫ (ro:if e_tst- e1- e2-)] ⇒ : (⊔ τ1 τ2)]]])
+   [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (⊔ τ1 τ2)]]])
 
 ;; TODO: fix this to support Racket parameter usage patterns?
 ;; eg, this wont work if applied since it's not a function type
 (define-typed-syntax make-parameter
   #;[(_ e) ⇐ : (~Param τ_expected) ≫
-   [⊢ [[e ≫ e-] ⇐ : τ_expected]]
+   [⊢ [e ≫ e- ⇐ : τ_expected]]
    --------
-   [⊢ [[_ ≫ (ro:make-parameter e-)]]]]
+   [⊢ [_ ≫ (ro:make-parameter e-)]]]
   [(_ e) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ]]
+   [⊢ [e ≫ e- ⇒ : τ]]
    --------
-   [⊢ [[_ ≫ (ro:make-parameter e-)] ⇒ : (Param τ)]]])
+   [⊢ [_ ≫ (ro:make-parameter e-) ⇒ : (Param τ)]]])
 
 (define-typed-syntax define #:datum-literals (: -> →)
   [(_ x:id e) ≫
    --------
    [_ ≻ (stlc:define x e)]]
   [(_ (f [x : ty] ... (~or → ->) ty_out) e) ≫
-;   [⊢ [[e ≫ e-] ⇒ : ty_e]]
+;   [⊢ [e ≫ e- ⇒ : ty_e]]
    [#:with f- (generate-temporary #'f)]
    --------
    [_ ≻ (begin-
@@ -113,15 +113,15 @@
 ;(define-rosette-primop bv : (→ Int BVPred BV)
 (define-typed-syntax bv
   [(_ e_val e_size) ≫
-   [⊢ [[e_val ≫ e_val-] ⇐ : Int]]
-   [⊢ [[e_size ≫ e_size-] ⇐ : BVPred]]
+   [⊢ [e_val ≫ e_val- ⇐ : Int]]
+   [⊢ [e_size ≫ e_size- ⇐ : BVPred]]
    --------
-   [⊢ [[_ ≫ (ro:bv e_val- e_size-)] ⇒ : BV]]]
+   [⊢ [_ ≫ (ro:bv e_val- e_size-) ⇒ : BV]]]
   [(_ e_val e_size) ≫
-   [⊢ [[e_val ≫ e_val-] ⇐ : Int]]
-   [⊢ [[e_size ≫ e_size-] ⇐ : Nat]]
+   [⊢ [e_val ≫ e_val- ⇐ : Int]]
+   [⊢ [e_size ≫ e_size- ⇐ : Nat]]
    --------
-   [⊢ [[_ ≫ (ro:bv e_val- e_size-)] ⇒ : BV]]])
+   [⊢ [_ ≫ (ro:bv e_val- e_size-) ⇒ : BV]]])
 
 (define-rosette-primop bv? : (→ BV Bool))
 (define-rosette-primop bitvector : (→ Nat BVPred))
@@ -147,27 +147,27 @@
 (define-typed-syntax bvand
   [f:id ≫ ; TODO: implement variable arity types
    --------
-   [⊢ [[_ ≫ ro:bvand] ⇒ : (→ BV BV BV)]]]
+   [⊢ [_ ≫ ro:bvand ⇒ : (→ BV BV BV)]]]
   [(_ e ...+) ≫
-   [⊢ [[e ≫ e-] ⇐ : BV] ...]
+   [⊢ [e ≫ e- ⇐ : BV] ...]
    --------
-   [⊢ [[_ ≫ (ro:bvand e- ...)] ⇒ : BV]]])
+   [⊢ [_ ≫ (ro:bvand e- ...) ⇒ : BV]]])
 (define-typed-syntax bvor
   [f:id ≫ ; TODO: implement variable arity types
    --------
-   [⊢ [[_ ≫ ro:bvor] ⇒ : (→ BV BV BV)]]]
+   [⊢ [_ ≫ ro:bvor ⇒ : (→ BV BV BV)]]]
   [(_ e ...+) ≫
-   [⊢ [[e ≫ e-] ⇐ : BV] ...]
+   [⊢ [e ≫ e- ⇐ : BV] ...]
    --------
-   [⊢ [[_ ≫ (ro:bvor e- ...)] ⇒ : BV]]])
+   [⊢ [_ ≫ (ro:bvor e- ...) ⇒ : BV]]])
 (define-typed-syntax bvxor
   [f:id ≫ ; TODO: implement variable arity types
    --------
-   [⊢ [[_ ≫ ro:bvxor] ⇒ : (→ BV BV BV)]]]
+   [⊢ [_ ≫ ro:bvxor ⇒ : (→ BV BV BV)]]]
   [(_ e ...+) ≫
-   [⊢ [[e ≫ e-] ⇐ : BV] ...]
+   [⊢ [e ≫ e- ⇐ : BV] ...]
    --------
-   [⊢ [[_ ≫ (ro:bvxor e- ...)] ⇒ : BV]]])
+   [⊢ [_ ≫ (ro:bvxor e- ...) ⇒ : BV]]])
 
 (define-rosette-primop bvshl : (→ BV BV BV))
 (define-rosette-primop bvlshr : (→ BV BV BV))
@@ -177,27 +177,27 @@
 (define-typed-syntax bvadd
   [f:id ≫ ; TODO: implement variable arity types
    --------
-   [⊢ [[_ ≫ ro:bvadd] ⇒ : (→ BV BV BV)]]]
+   [⊢ [_ ≫ ro:bvadd ⇒ : (→ BV BV BV)]]]
   [(_ e ...+) ≫
-   [⊢ [[e ≫ e-] ⇐ : BV] ...]
+   [⊢ [e ≫ e- ⇐ : BV] ...]
    --------
-   [⊢ [[_ ≫ (ro:bvadd e- ...)] ⇒ : BV]]])
+   [⊢ [_ ≫ (ro:bvadd e- ...) ⇒ : BV]]])
 (define-typed-syntax bvsub
   [f:id ≫ ; TODO: implement variable arity types
    --------
-   [⊢ [[_ ≫ ro:bvsub] ⇒ : (→ BV BV BV)]]]
+   [⊢ [_ ≫ ro:bvsub ⇒ : (→ BV BV BV)]]]
   [(_ e ...+) ≫
-   [⊢ [[e ≫ e-] ⇐ : BV] ...]
+   [⊢ [e ≫ e- ⇐ : BV] ...]
    --------
-   [⊢ [[_ ≫ (ro:bvsub e- ...)] ⇒ : BV]]])
+   [⊢ [_ ≫ (ro:bvsub e- ...) ⇒ : BV]]])
 (define-typed-syntax bvmul
   [f:id ≫ ; TODO: implement variable arity types
    --------
-   [⊢ [[_ ≫ ro:bvmul] ⇒ : (→ BV BV BV)]]]
+   [⊢ [_ ≫ ro:bvmul ⇒ : (→ BV BV BV)]]]
   [(_ e ...+) ≫
-   [⊢ [[e ≫ e-] ⇐ : BV] ...]
+   [⊢ [e ≫ e- ⇐ : BV] ...]
    --------
-   [⊢ [[_ ≫ (ro:bvmul e- ...)] ⇒ : BV]]])
+   [⊢ [_ ≫ (ro:bvmul e- ...) ⇒ : BV]]])
 
 (define-rosette-primop bvsdiv : (→ BV BV BV))
 (define-rosette-primop bvudiv : (→ BV BV BV))
@@ -207,9 +207,9 @@
 
 (define-typed-syntax concat
   [(_ e ...+) ≫
-   [⊢ [[e ≫ e-] ⇐ : BV] ...]
+   [⊢ [e ≫ e- ⇐ : BV] ...]
    --------
-   [⊢ [[_ ≫ (ro:concat e- ...)] ⇒ : BV]]])
+   [⊢ [_ ≫ (ro:concat e- ...) ⇒ : BV]]])
 
 (define-rosette-primop extract : (→ Int Int BV BV))
 ;; TODO: additionally support union in 2nd arg
diff --git a/turnstile/examples/stlc+box.rkt b/turnstile/examples/stlc+box.rkt
index d6427c2..19eeb4e 100644
--- a/turnstile/examples/stlc+box.rkt
+++ b/turnstile/examples/stlc+box.rkt
@@ -13,20 +13,20 @@
 
 (define-typed-syntax ref
   [(ref e) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ]]
+   [⊢ [e ≫ e- ⇒ : τ]]
    --------
-   [⊢ [[_ ≫ (box- e-)] ⇒ : (Ref τ)]]])
+   [⊢ [_ ≫ (box- e-) ⇒ : (Ref τ)]]])
 
 (define-typed-syntax deref
   [(deref e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~Ref τ)]]
+   [⊢ [e ≫ e- ⇒ : (~Ref τ)]]
    --------
-   [⊢ [[_ ≫ (unbox- e-)] ⇒ : τ]]])
+   [⊢ [_ ≫ (unbox- e-) ⇒ : τ]]])
 
 (define-typed-syntax := #:literals (:=)
   [(:= e_ref e) ≫
-   [⊢ [[e_ref ≫ e_ref-] ⇒ : (~Ref τ)]]
-   [⊢ [[e ≫ e-] ⇐ : τ]]
+   [⊢ [e_ref ≫ e_ref- ⇒ : (~Ref τ)]]
+   [⊢ [e ≫ e- ⇐ : τ]]
    --------
-   [⊢ [[_ ≫ (set-box!- e_ref- e-)] ⇒ : Unit]]])
+   [⊢ [_ ≫ (set-box!- e_ref- e-) ⇒ : Unit]]])
 
diff --git a/turnstile/examples/stlc+cons.rkt b/turnstile/examples/stlc+cons.rkt
index f2d333e..024e0fe 100644
--- a/turnstile/examples/stlc+cons.rkt
+++ b/turnstile/examples/stlc+cons.rkt
@@ -15,67 +15,67 @@
 (define-typed-syntax nil
   [(nil ~! τi:type-ann) ≫
    --------
-   [⊢ [[_ ≫ null-] ⇒ : (List τi.norm)]]]
+   [⊢ [_ ≫ null- ⇒ : (List τi.norm)]]]
   ; minimal type inference
   [nil:id ⇐ : (~List τ) ≫
    --------
-   [⊢ [[_ ≫ null-] ⇐ : _]]])
+   [⊢ [_ ≫ null- ⇐ : _]]])
 (define-typed-syntax cons
   [(cons e1 e2) ≫
-   [⊢ [[e1 ≫ e1-] ⇒ : τ1]]
-   [⊢ [[e2 ≫ e2-] ⇐ : (List τ1)]]
+   [⊢ [e1 ≫ e1- ⇒ : τ1]]
+   [⊢ [e2 ≫ e2- ⇐ : (List τ1)]]
    --------
-   [⊢ [[_ ≫ (cons- e1- e2-)] ⇒ : (List τ1)]]])
+   [⊢ [_ ≫ (cons- e1- e2-) ⇒ : (List τ1)]]])
 (define-typed-syntax isnil
   [(isnil e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~List _)]]
+   [⊢ [e ≫ e- ⇒ : (~List _)]]
    --------
-   [⊢ [[_ ≫ (null?- e-)] ⇒ : Bool]]])
+   [⊢ [_ ≫ (null?- e-) ⇒ : Bool]]])
 (define-typed-syntax head
   [(head e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
+   [⊢ [e ≫ e- ⇒ : (~List τ)]]
    --------
-   [⊢ [[_ ≫ (car- e-)] ⇒ : τ]]])
+   [⊢ [_ ≫ (car- e-) ⇒ : τ]]])
 (define-typed-syntax tail
   [(tail e) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ-lst]]
+   [⊢ [e ≫ e- ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
-   [⊢ [[_ ≫ (cdr- e-)] ⇒ : τ-lst]]])
+   [⊢ [_ ≫ (cdr- e-) ⇒ : τ-lst]]])
 (define-typed-syntax list
   [(list) ≫
    --------
    [_ ≻ nil]]
   [(list x . rst) ⇐ : (~List τ) ≫ ; has expected type
    --------
-   [⊢ [[_ ≫ (cons (add-expected x τ) (list . rst))] ⇐ : _]]]
+   [⊢ [_ ≫ (cons (add-expected x τ) (list . rst)) ⇐ : _]]]
   [(list x . rst) ≫ ; no expected type
    --------
    [_ ≻ (cons x (list . rst))]])
 (define-typed-syntax reverse
   [(reverse e) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ-lst]]
+   [⊢ [e ≫ e- ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
-   [⊢ [[_ ≫ (reverse- e-)] ⇒ : τ-lst]]])
+   [⊢ [_ ≫ (reverse- e-) ⇒ : τ-lst]]])
 (define-typed-syntax length
   [(length e) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ-lst]]
+   [⊢ [e ≫ e- ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
-   [⊢ [[_ ≫ (length- e-)] ⇒ : Int]]])
+   [⊢ [_ ≫ (length- e-) ⇒ : Int]]])
 (define-typed-syntax list-ref
   [(list-ref e n) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
-   [⊢ [[n ≫ n-] ⇐ : Int]]
+   [⊢ [e ≫ e- ⇒ : (~List τ)]]
+   [⊢ [n ≫ n- ⇐ : Int]]
    --------
-   [⊢ [[_ ≫ (list-ref- e- n-)] ⇒ : τ]]])
+   [⊢ [_ ≫ (list-ref- e- n-) ⇒ : τ]]])
 (define-typed-syntax member
   [(member v e) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
-   [⊢ [[v ≫ v-] ⇐ : τ]]
+   [⊢ [e ≫ e- ⇒ : (~List τ)]]
+   [⊢ [v ≫ v- ⇐ : τ]]
    --------
-   [⊢ [[_ ≫ (member- v- e-)] ⇒ : Bool]]])
+   [⊢ [_ ≫ (member- v- e-) ⇒ : Bool]]])
diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt
index e365c4c..f29b842 100644
--- a/turnstile/examples/stlc+effect.rkt
+++ b/turnstile/examples/stlc+effect.rkt
@@ -30,7 +30,7 @@
 
 (define-typed-syntax effect:#%app #:export-as #%app
   [(_ efn e ...) ≫
-   [⊢ [[efn ≫ e_fn-]
+   [⊢ [efn ≫ e_fn-
        (⇒ : (~→ τ_in ... τ_out)
           (⇒ ν (~locs tyns ...))
           (⇒ := (~locs tyas ...))
@@ -40,14 +40,14 @@
        (⇒ ! (~locs fds ...))]]
    [#:fail-unless (stx-length=? #'[e ...] #'[τ_in ...])
     (num-args-fail-msg #'efn #'[τ_in ...] #'[e ...])]
-   [⊢ [[e ≫ e_arg-]
+   [⊢ [e ≫ e_arg-
        (⇐ : τ_in)
        (⇒ ν (~locs ns ...))
        (⇒ := (~locs as ...))
        (⇒ ! (~locs ds ...))]
       ...]
    --------
-   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)]
+   [⊢ [_ ≫ (#%app- e_fn- e_arg- ...)
        (⇒ : τ_out)
        (⇒ ν (locs fns ... tyns ... ns ... ...))
        (⇒ := (locs fas ... tyas ... as ... ...))
@@ -55,14 +55,14 @@
 
 (define-typed-syntax λ
   [(λ bvs:type-ctx e) ≫
-   [() ([bvs.x : bvs.type ≫ x-] ...) ⊢
-       [[e ≫ e-]
+   [() ([bvs.x ≫ x- : bvs.type] ...) ⊢
+       [e ≫ e-
         (⇒ : τ_res)
         (⇒ ν (~locs ns ...))
         (⇒ := (~locs as ...))
         (⇒ ! (~locs ds ...))]]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) e-)]
+   [⊢ [_ ≫ (λ- (x- ...) e-)
        (⇒ : (→ bvs.type ... τ_res)
           (⇒ ν (locs ns ...))
           (⇒ := (locs as ...))
@@ -72,44 +72,44 @@
 
 (define-typed-syntax ref
   [(ref e) ≫
-   [⊢ [[e ≫ e-]
+   [⊢ [e ≫ e-
        (⇒ : τ)
        (⇒ ν (~locs ns ...))
        (⇒ := (~locs as ...))
        (⇒ ! (~locs ds ...))]]
    --------
-   [⊢ [[_ ≫ (box- e-)]
+   [⊢ [_ ≫ (box- e-)
        (⇒ : (Ref τ))
        (⇒ ν (locs #,(syntax-position stx) ns ...))
        (⇒ := (locs as ...))
        (⇒ ! (locs ds ...))]]])
 (define-typed-syntax deref
   [(deref e) ≫
-   [⊢ [[e ≫ e-]
+   [⊢ [e ≫ e-
        (⇒ : (~Ref ty))
        (⇒ ν (~locs ns ...))
        (⇒ := (~locs as ...))
        (⇒ ! (~locs ds ...))]]
    --------
-   [⊢ [[_ ≫ (unbox- e-)]
+   [⊢ [_ ≫ (unbox- e-)
        (⇒ : ty)
        (⇒ ν (locs ns ...))
        (⇒ := (locs as ...))
        (⇒ ! (locs #,(syntax-position stx) ds ...))]]])
 (define-typed-syntax := #:literals (:=)
   [(:= e_ref e) ≫
-   [⊢ [[e_ref ≫ e_ref-]
+   [⊢ [e_ref ≫ e_ref-
        (⇒ : (~Ref ty))
        (⇒ ν (~locs ns1 ...))
        (⇒ := (~locs as1 ...))
        (⇒ ! (~locs ds1 ...))]]
-   [⊢ [[e ≫ e-]
+   [⊢ [e ≫ e-
        (⇐ : ty)
        (⇒ ν (~locs ns2 ...))
        (⇒ := (~locs as2 ...))
        (⇒ ! (~locs ds2 ...))]]
    --------
-   [⊢ [[_ ≫ (set-box!- e_ref- e-)]
+   [⊢ [_ ≫ (set-box!- e_ref- e-)
        (⇒ : Unit)
        (⇒ ν (locs ns1 ... ns2 ...))
        (⇒ := (locs #,(syntax-position stx) as1 ... as2 ...))
diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt
index d6e4215..ddc88e0 100644
--- a/turnstile/examples/stlc+lit.rkt
+++ b/turnstile/examples/stlc+lit.rkt
@@ -35,7 +35,7 @@
 (define-typed-syntax #%datum
   [(#%datum . n:integer) ≫
    --------
-   [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Int]]]
+   [⊢ [_ ≫ (#%datum- . n) ⇒ : Int]]]
   [(_ . x) ≫
    --------
    [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
diff --git a/turnstile/examples/stlc+rec-iso.rkt b/turnstile/examples/stlc+rec-iso.rkt
index 2489692..05fa936 100644
--- a/turnstile/examples/stlc+rec-iso.rkt
+++ b/turnstile/examples/stlc+rec-iso.rkt
@@ -39,13 +39,13 @@
 (define-typed-syntax unfld
   [(unfld τ:type-ann e) ≫
    [#:with (~μ* (tv) τ_body) #'τ.norm]
-   [⊢ [[e ≫ e-] ⇐ : τ.norm]]
+   [⊢ [e ≫ e- ⇐ : τ.norm]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : #,(subst #'τ.norm #'tv #'τ_body)]]])
+   [⊢ [_ ≫ e- ⇒ : #,(subst #'τ.norm #'tv #'τ_body)]]])
 (define-typed-syntax fld
   [(fld τ:type-ann e) ≫
    [#:with (~μ* (tv) τ_body) #'τ.norm]
    [#:with τ_e (subst #'τ.norm #'tv #'τ_body)]
-   [⊢ [[e ≫ e-] ⇐ : τ_e]]
+   [⊢ [e ≫ e- ⇐ : τ_e]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : τ.norm]]])
+   [⊢ [_ ≫ e- ⇒ : τ.norm]]])
diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt
index 69dfb40..cbcd295 100644
--- a/turnstile/examples/stlc+reco+var.rkt
+++ b/turnstile/examples/stlc+reco+var.rkt
@@ -31,14 +31,14 @@
 (define-typed-syntax define
   [(define x:id : τ:type e:expr) ≫
    ;This wouldn't work with mutually recursive definitions
-   ;[⊢ [[e ≫ e-] ⇐ τ.norm]]
+   ;[⊢ [e ≫ e- ⇐ τ.norm]]
    ;So expand to an ann form instead.
    --------
    [_ ≻ (begin-
           (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
           (define- y (ann e : τ.norm)))]]
   [(define x:id e) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ]]
+   [⊢ [e ≫ e- ⇒ : τ]]
    [#:with y (generate-temporary #'x)]
    --------
    [_ ≻ (begin-
@@ -89,18 +89,18 @@
 ;; records
 (define-typed-syntax tup #:datum-literals (=)
   [(tup [l:id = e] ...) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ] ...]
+   [⊢ [e ≫ e- ⇒ : τ] ...]
    --------
-   [⊢ [[_ ≫ (list- (list- 'l e-) ...)] ⇒ : (× [l : τ] ...)]]])
+   [⊢ [_ ≫ (list- (list- 'l e-) ...) ⇒ : (× [l : τ] ...)]]])
 (define-typed-syntax proj #:literals (quote)
   [(proj e_rec l:id) ≫
-   [⊢ [[e_rec ≫ e_rec-] ⇒ : τ_e]]
+   [⊢ [e_rec ≫ e_rec- ⇒ : τ_e]]
    [#:fail-unless (×? #'τ_e)
     (format "Expected expression ~s to have × type, got: ~a"
             (syntax->datum #'e_rec) (type->str #'τ_e))]
    [#:with τ_l (×-ref #'τ_e #'l)]
    --------
-   [⊢ [[_ ≫ (cadr- (assoc- 'l e_rec-))] ⇒ : τ_l]]])
+   [⊢ [_ ≫ (cadr- (assoc- 'l e_rec-)) ⇒ : τ_l]]])
 
 (define-type-constructor ∨/internal #:arity >= 0)
 
@@ -157,20 +157,20 @@
            (λ () (raise-syntax-error #f
                     (format "~a field does not exist" (syntax->datum #'l))
                     stx)))]
-   [⊢ [[e ≫ e-] ⇐ : τ_e]]
+   [⊢ [e ≫ e- ⇐ : τ_e]]
    --------
-   [⊢ [[_ ≫ (list- 'l e)] ⇐ : _]]])
+   [⊢ [_ ≫ (list- 'l e) ⇐ : _]]])
 
 (define-typed-syntax case
   #:datum-literals (of =>)
   [(case e [l:id x:id => e_l] ...) ≫
    [#:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"]
-   [⊢ [[e ≫ e-] ⇒ : (~∨* [l_x : τ_x] ...)]]
+   [⊢ [e ≫ e- ⇒ : (~∨* [l_x : τ_x] ...)]]
    [#:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"]
    [#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"]
-   [() ([x : τ_x ≫ x-]) ⊢ [[e_l ≫ e_l-] ⇒ : τ_el]] ...
+   [() ([x ≫ x- : τ_x]) ⊢ [e_l ≫ e_l- ⇒ : τ_el]] ...
    --------
-   [⊢ [[_ ≫
-        (let- ([l_e (car- e-)])
-          (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))]
-       ⇒ : (⊔ τ_el ...)]]])
+   [⊢ [_ ≫
+         (let- ([l_e (car- e-)])
+               (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))
+         ⇒ : (⊔ τ_el ...)]]])
diff --git a/turnstile/examples/stlc+sub.rkt b/turnstile/examples/stlc+sub.rkt
index f634075..b2493c0 100644
--- a/turnstile/examples/stlc+sub.rkt
+++ b/turnstile/examples/stlc+sub.rkt
@@ -30,13 +30,13 @@
 (define-typed-syntax #%datum
   [(#%datum . n:nat) ≫
    --------
-   [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Nat]]]
+   [⊢ [_ ≫ (#%datum- . n) ⇒ : Nat]]]
   [(#%datum . n:integer) ≫
    --------
-   [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Int]]]
+   [⊢ [_ ≫ (#%datum- . n) ⇒ : Int]]]
   [(#%datum . n:number) ≫
    --------
-   [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Num]]]
+   [⊢ [_ ≫ (#%datum- . n) ⇒ : Num]]]
   [(#%datum . x) ≫
    --------
    [_ ≻ (ext:#%datum . x)]])
diff --git a/turnstile/examples/stlc+tup.rkt b/turnstile/examples/stlc+tup.rkt
index 4589865..75adea4 100644
--- a/turnstile/examples/stlc+tup.rkt
+++ b/turnstile/examples/stlc+tup.rkt
@@ -18,18 +18,18 @@
 (define-typed-syntax tup
   [(tup e ...) ⇐ : (~× τ ...) ≫
    [#:when (stx-length=? #'[e ...] #'[τ ...])]
-   [⊢ [[e ≫ e-] ⇐ : τ] ...]
+   [⊢ [e ≫ e- ⇐ : τ] ...]
    --------
-   [⊢ [[_ ≫ (list- e- ...)] ⇐ : _]]]
+   [⊢ [_ ≫ (list- e- ...) ⇐ : _]]]
   [(tup e ...) ≫
-   [⊢ [[e ≫ e-] ⇒ : τ] ...]
+   [⊢ [e ≫ e- ⇒ : τ] ...]
    --------
-   [⊢ [[_ ≫ (list- e- ...)] ⇒ : (× τ ...)]]])
+   [⊢ [_ ≫ (list- e- ...) ⇒ : (× τ ...)]]])
 
 (define-typed-syntax proj
   [(proj e_tup n:nat) ≫
-   [⊢ [[e_tup ≫ e_tup-] ⇒ : (~× τ ...)]]
+   [⊢ [e_tup ≫ e_tup- ⇒ : (~× τ ...)]]
    [#:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large"]
    --------
-   [⊢ [[_ ≫ (list-ref- e_tup- n)] ⇒ : #,(stx-list-ref #'[τ ...] (syntax-e #'n))]]])
+   [⊢ [_ ≫ (list-ref- e_tup- n) ⇒ : #,(stx-list-ref #'[τ ...] (syntax-e #'n))]]])
 
diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
index 22f8a8f..4cbace5 100644
--- a/turnstile/examples/stlc.rkt
+++ b/turnstile/examples/stlc.rkt
@@ -29,25 +29,25 @@
 
 (define-typed-syntax λ #:datum-literals (:)
   [(λ ([x:id : τ_in:type] ...) e) ≫
-   [() ([x : τ_in.norm ≫ x-] ...) ⊢ [[e ≫ e-] ⇒ : τ_out]]
+   [() ([x ≫ x- : τ_in.norm] ...) ⊢ [e ≫ e- ⇒ : τ_out]]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇒ : (→ τ_in.norm ... τ_out)]]]
+   [⊢ [_ ≫ (λ- (x- ...) e-) ⇒ : (→ τ_in.norm ... τ_out)]]]
   [(λ (x:id ...) e) ⇐ : (~→ τ_in ... τ_out) ≫
-   [() ([x : τ_in ≫ x-] ...) ⊢ [[e ≫ e-] ⇐ : τ_out]]
+   [() ([x ≫ x- : τ_in] ...) ⊢ [e ≫ e- ⇐ : τ_out]]
    --------
-   [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇐ : _]]])
+   [⊢ [_ ≫ (λ- (x- ...) e-) ⇐ : _]]])
 
 (define-typed-syntax #%app
   [(_ e_fn e_arg ...) ≫
-   [⊢ [[e_fn ≫ e_fn-] ⇒ : (~→ τ_in ... τ_out)]]
+   [⊢ [e_fn ≫ e_fn- ⇒ : (~→ τ_in ... τ_out)]]
    [#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
     (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])]
-   [⊢ [[e_arg ≫ e_arg-] ⇐ : τ_in] ...]
+   [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
    --------
-   [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out]]])
+   [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
 
 (define-typed-syntax ann #:datum-literals (:)
   [(ann e : τ:type) ≫
-   [⊢ [[e ≫ e-] ⇐ : τ.norm]]
+   [⊢ [e ≫ e- ⇐ : τ.norm]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : τ.norm]]])
+   [⊢ [_ ≫ e- ⇒ : τ.norm]]])
diff --git a/turnstile/examples/sysf.rkt b/turnstile/examples/sysf.rkt
index 762e8bf..aa583a0 100644
--- a/turnstile/examples/sysf.rkt
+++ b/turnstile/examples/sysf.rkt
@@ -16,16 +16,16 @@
 
 (define-typed-syntax Λ
   [(Λ (tv:id ...) e) ≫
-   [([tv : #%type ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ : τ]]
+   [([tv ≫ tv- : #%type] ...) () ⊢ [e ≫ e- ⇒ : τ]]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : (∀ (tv- ...) τ)]]])
+   [⊢ [_ ≫ e- ⇒ : (∀ (tv- ...) τ)]]])
 
 (define-typed-syntax inst
   [(inst e τ:type ...) ≫
-   [⊢ [[e ≫ e-] ⇒ : (~∀ tvs τ_body)]]
+   [⊢ [e ≫ e- ⇒ : (~∀ tvs τ_body)]]
    [#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)]
    --------
-   [⊢ [[_ ≫ e-] ⇒ : τ_inst]]]
+   [⊢ [_ ≫ e- ⇒ : τ_inst]]]
   [(inst e) ≫
    --------
    [_ ≻ e]])
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
index 4ebfb0d..a7ee57e 100644
--- a/turnstile/turnstile.rkt
+++ b/turnstile/turnstile.rkt
@@ -132,10 +132,10 @@
   (define-splicing-syntax-class id+props+≫
     #:datum-literals (≫)
     #:attributes ([x- 1] [ctx 1])
-    [pattern (~seq [x:id props:props ≫ x--:id])
+    [pattern (~seq [x:id ≫ x--:id props:props])
              #:with [x- ...] #'[x--]
              #:with [ctx ...] #'[[x props.stuff ...]]]
-    [pattern (~seq [x:id props:props ≫ x--:id] ooo:elipsis)
+    [pattern (~seq [x:id ≫ x--:id props:props] ooo:elipsis)
              #:with [x- ...] #'[x-- ooo]
              #:with [ctx ...] #'[[x props.stuff ...] ooo]])
   (define-splicing-syntax-class id-props+≫*
@@ -146,7 +146,7 @@
   (define-splicing-syntax-class inf
     #:datum-literals (⊢ ⇒ ⇐ ≫ :)
     #:attributes (depth es-stx es-stx-orig es-pat)
-    [pattern (~seq [[e-stx* ≫ e-pat*] props:⇒-props] ooo:elipsis ...)
+    [pattern (~seq [e-stx* ≫ e-pat* props:⇒-props] ooo:elipsis ...)
              #:with depth (stx-length #'[ooo ...])
              #:with es-stx (with-depth #'e-stx* #'[ooo ...])
              #:with es-stx-orig (with-depth #'e-stx* #'[ooo ...])
@@ -156,7 +156,7 @@
                    #'(~and props.e-pat
                            e-pat*)
                    #'[ooo ...]))]
-    [pattern (~seq [[e-stx* ≫ e-pat*] props:⇐-props] ooo:elipsis ...)
+    [pattern (~seq [e-stx* ≫ e-pat* props:⇐-props] ooo:elipsis ...)
              #:with e-tmp (generate-temporary #'e-pat*)
              #:with τ-tmp (generate-temporary 'τ)
              #:with τ-exp-tmp (generate-temporary 'τ_expected)
@@ -247,7 +247,7 @@
   (define-syntax-class last-clause
     #:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
     #:attributes ([pat 0] [stuff 1] [body 0])
-    [pattern [⊢ [[pat ≫ e-stx] props:⇒-props/conclusion]]
+    [pattern [⊢ [pat ≫ e-stx props:⇒-props/conclusion]]
              #:with [stuff ...] #'[]
              #:with body:expr
              (for/fold ([body #'(quasisyntax/loc this-syntax e-stx)])
@@ -255,9 +255,9 @@
                         [v (in-list (syntax->list #'[props.tag-expr ...]))])
                (with-syntax ([body body] [k k] [v v])
                  #'(assign-type body #:tag 'k v)))]
-    [pattern [⊢ [[e-stx]]]
-             #:with :last-clause #'[⊢ [[_ ≫ e-stx] ⇐ : _]]]
-    [pattern [⊢ [[pat* ≫ e-stx] ⇐ : τ-pat]]
+    [pattern [⊢ [e-stx]]
+             #:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
+    [pattern [⊢ [pat* ≫ e-stx ⇐ : τ-pat]]
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)
              #:with pat