diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
index ff2b31a..26d5127 100644
--- a/turnstile/examples/stlc.rkt
+++ b/turnstile/examples/stlc.rkt
@@ -12,25 +12,25 @@
 
 (define-typed-syntax λ #:datum-literals (:)
   [(λ ([x:id : τ_in:type] ...) e) ≫
-   [([x ≫ x- : τ_in.norm] ...) ⊢ [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 ≫ x- : τ_in] ...) ⊢ [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] ...]
    --------
-   [⊢ [_ ≫ (#%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/turnstile.rkt b/turnstile/turnstile.rkt
index 4b7fa90..4ebda62 100644
--- a/turnstile/turnstile.rkt
+++ b/turnstile/turnstile.rkt
@@ -161,7 +161,8 @@
   (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 (~or (~seq e-stx* ≫ e-pat* props:⇒-props (~parse (ooo ...) #'()))
+                  (~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 ...])
@@ -171,7 +172,8 @@
                    #'(~and props.e-pat
                            e-pat*)
                    #'[ooo ...]))]
-    [pattern (~seq [e-stx* ≫ e-pat* props:⇐-props] ooo:elipsis ...)
+    [pattern (~or (~seq e-stx* ≫ e-pat* props:⇐-props (~parse (ooo ...) #'()))
+                  (~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)
@@ -208,6 +210,8 @@
     #:datum-literals (⊢)
     [pattern (~or (~seq [⊢ inf:inf*] ooo:elipsis ...
                         (~parse ((ctx.x- ctx.ctx tvctx.x- tvctx.ctx) ...) #'()))
+                  (~seq [ctx:id-props+≫* ⊢ inf:inf*] ooo:elipsis ...
+                        (~parse ((tvctx.x- tvctx.ctx) ...) #'()))
                   (~seq [(ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis ...
                         (~parse ((tvctx.x- tvctx.ctx) ...) #'()))
                   (~seq [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis ...))
@@ -270,7 +274,8 @@
   (define-syntax-class last-clause
     #:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
     #:attributes ([pat 0] [stuff 1] [body 0])
-    [pattern [⊢ [pat ≫ e-stx props:⇒-props/conclusion]]
+    [pattern (~or [⊢ pat ≫ e-stx props:⇒-props/conclusion]
+                  [⊢ [pat ≫ e-stx props:⇒-props/conclusion]])
              #:with [stuff ...] #'[]
              #:with body:expr
              (for/fold ([body #'(quasisyntax/loc this-syntax e-stx)])
@@ -278,9 +283,11 @@
                         [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]]
+    [pattern (~or [⊢ [e-stx]] [⊢ (~and e-stx (~not [_ ≫ . rst]))])
              #:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
-    [pattern (~or [⊢ [pat* ≫ e-stx ⇐ τ-pat]]
+    [pattern (~or [⊢ pat* ≫ e-stx ⇐ τ-pat]
+                  [⊢ pat* ≫ e-stx ⇐ : τ-pat]
+                  [⊢ [pat* ≫ e-stx ⇐ τ-pat]]
                   [⊢ [pat* ≫ e-stx ⇐ : τ-pat]])
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)