diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
index c87227b..cbd32f9 100644
--- a/turnstile/examples/rosette/rosette2.rkt
+++ b/turnstile/examples/rosette/rosette2.rkt
@@ -1,10 +1,13 @@
 #lang turnstile
-(extends "../stlc.rkt")
+(extends "../stlc.rkt"
+  #:except #%app)
 (reuse #%datum #:from "../stlc+union.rkt")
 (reuse define-type-alias #:from "../stlc+reco+var.rkt")
 (reuse define-named-type-alias #:from "../stlc+union.rkt")
 
 (provide CU U
+         C→
+         Ccase->
          CNegInt NegInt
          CZero Zero
          CPosInt PosInt
@@ -16,11 +19,22 @@
          CString ; symbolic string are not supported
          )
 
-(require 
+(require
+ (prefix-in ro: rosette)
  (only-in "../stlc+union.rkt" define-named-type-alias prune+sort current-sub?)
  (prefix-in C (only-in "../stlc+union+case.rkt"
-                       PosInt Zero NegInt Float Bool String [U U*] U*? case-> →))
- (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]))
+                       PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?))
+ (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
+ (only-in "../ext-stlc.rkt" define-primop))
+
+;; copied from rosette.rkt
+(define-simple-macro (define-rosette-primop op:id : ty)
+  (begin
+    (require (only-in rosette [op op]))
+    (define-primop op : ty)))
+
+;; ---------------------------------
+;; Concrete and Symbolic union types
 
 (define-syntax (CU stx)
   (syntax-parse stx
@@ -44,6 +58,23 @@
   (define (concrete? t)
     (not (U*? t))))
 
+;; ---------------------------------
+;; case-> and Ccase->
+
+;; Ccase-> must check that its subparts are concrete → types
+(define-syntax (Ccase-> stx)
+  (syntax-parse stx
+    [(_ . tys)
+     #:with tys+ (stx-map (current-type-eval) #'tys)
+     #:fail-unless (stx-andmap →? #'tys+)
+                   "CU require concrete arguments"
+     #'(Ccase->* . tys+)]))
+
+;; TODO: What should case-> do when given symbolic function
+;; types? Should it transform (case-> (U (C→ τ ...)) ...)
+;; into (U (Ccase-> (C→ τ ...) ...)) ? What makes sense here?
+
+
 ;; ---------------------------------
 ;; Symbolic versions of types
 
@@ -69,6 +100,66 @@
 (define-symbolic-named-type-alias Num (CU CFloat CInt))
 
 ;; ---------------------------------
+;; Function Application
+
+;; copied from rosette.rkt
+(define-typed-syntax app #:export-as #%app
+  [(_ e_fn e_arg ...) ≫
+   [⊢ [e_fn ≫ e_fn- ⇒ : (~C→ ~! τ_in ... τ_out)]]
+   #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+   (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+   [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
+   --------
+   [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]
+  [(_ e_fn e_arg ...) ≫
+   [⊢ [e_fn ≫ e_fn- ⇒ : (~Ccase-> ~! . (~and ty_fns ((~C→ . _) ...)))]]
+   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+   #:with τ_out
+   (for/first ([ty_f (stx->list #'ty_fns)]
+               #:when (syntax-parse ty_f
+                        [(~C→ τ_in ... τ_out)
+                         (and (stx-length=? #'(τ_in ...) #'(e_arg ...))
+                              (typechecks? #'(τ_arg ...) #'(τ_in ...)))]))
+     (syntax-parse ty_f [(~C→ _ ... t_out) #'t_out]))
+   #:fail-unless (syntax-e #'τ_out)
+   ; use (failing) typechecks? to get err msg
+   (syntax-parse #'ty_fns
+     [((~C→ τ_in ... _) ...)
+      (let* ([τs_expecteds #'((τ_in ...) ...)]
+             [τs_given #'(τ_arg ...)]
+             [expressions #'(e_arg ...)])
+        (format (string-append "type mismatch\n"
+                               "  expected one of:\n"
+                               "    ~a\n"
+                               "  given: ~a\n"
+                               "  expressions: ~a")
+         (string-join
+          (stx-map
+           (lambda (τs_expected)
+             (string-join (stx-map type->str τs_expected) ", "))
+           τs_expecteds)
+          "\n    ")
+           (string-join (stx-map type->str τs_given) ", ")
+           (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))])
+   --------
+   [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]])
+
+;; ---------------------------------
+;; Types for built-in operations
+
+(define-rosette-primop add1 : (Ccase-> (C→ CNegInt (CU CNegInt CZero))
+                                       (C→ NegInt (U NegInt Zero))
+                                       (C→ CZero CPosInt)
+                                       (C→ Zero PosInt)
+                                       (C→ CPosInt CPosInt)
+                                       (C→ PosInt PosInt)
+                                       (C→ CNat CPosInt)
+                                       (C→ Nat PosInt)
+                                       (C→ CInt CInt)
+                                       (C→ Int Int)))
+
+;; ---------------------------------
+;; Subtyping
 
 (begin-for-syntax
   (define (sub? t1 t2)
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
index 56f1d24..77e87e0 100644
--- a/turnstile/examples/tests/rosette/rosette2-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -58,6 +58,20 @@
 (check-type     ((λ ([x : (U Int Bool)]) x) ((λ ([x : (U CInt CBool)]) x) 1)) : (U CInt CBool))
 (check-type     ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (U Int Bool)]) x) 1)) : (U CInt CBool))
 
+;; add1 has a case-> type with cases for different subtypes of Int
+;; to preserve some of the type information through the operation
+(check-type (add1 9) : CPosInt -> 10)
+(check-type (add1 0) : CPosInt -> 1)
+(check-type (add1 -1) : (CU CNegInt CZero) -> 0)
+(check-type (add1 -9) : (CU CNegInt CZero) -> -8)
+(check-type (add1 (ann 9 : PosInt)) : PosInt -> 10)
+(check-type (add1 (ann 0 : Zero)) : PosInt -> 1)
+(check-type (add1 (ann 9 : Nat)) : PosInt -> 10)
+(check-type (add1 (ann 0 : Nat)) : PosInt -> 1)
+(check-type (add1 (ann -1 : NegInt)) : (U NegInt Zero) -> 0)
+(check-type (add1 (ann -9 : NegInt)) : (U NegInt Zero) -> -8)
+(check-type (add1 (ann 9 : Int)) : Int -> 10)
+
 ;; (check-type (sub1 10) : Nat -> 9)
 ;; (check-type (sub1 0) : NegInt -> -1)
 ;; (check-type (sub1 -1) : NegInt -> -2)
@@ -167,18 +181,18 @@
 ;;               (if c (bitvector 5) (bitvector 6))) 
 ;;   : BV -> (if c (bv 3 5) (bv 3 6)))
 
-;; ;; case-> subtyping
-;; (check-type ((λ ([f : (→ Int Int)]) (f 10)) add1) : Int -> 11)
-;; (check-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Int -> 11)
-;; (check-type ((λ ([f : (case-> (→ Nat Nat)
-;;                               (→ Int Int))]) (f 10)) add1) : Int -> 11)
-;; (check-not-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Nat)
-;; (check-type ((λ ([f : (case-> (→ Nat Nat)
-;;                               (→ Int Int))]) (f 10)) add1) : Nat -> 11)
-;; (typecheck-fail ((λ ([f : (case-> (→ Zero Zero)
-;;                                   (→ Int Int))]) (f 10)) add1) 
-;;  #:with-msg
-;;  (string-append "expected \\(case-> \\(→ Zero Zero\\) \\(→ Int Int\\)\\), "
-;;                 "given \\(case-> \\(→ NegInt \\(U NegInt Zero\\)\\) \\(→ Zero PosInt\\) "
-;;                 "\\(→ PosInt PosInt\\) \\(→ Nat PosInt\\) \\(→ Int Int\\)\\)"))
+;; case-> subtyping
+(check-type ((λ ([f : (C→ Int Int)]) (f 10)) add1) : Int -> 11)
+(check-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Int -> 11)
+(check-type ((λ ([f : (Ccase-> (C→ Nat Nat)
+                               (C→ Int Int))]) (f 10)) add1) : Int -> 11)
+(check-not-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Nat)
+(check-type ((λ ([f : (Ccase-> (C→ Nat Nat)
+                               (C→ Int Int))]) (f 10)) add1) : Nat -> 11)
+(typecheck-fail ((λ ([f : (Ccase-> (C→ Zero Zero)
+                                   (C→ Int Int))]) (f 10)) add1) 
+  #:with-msg
+  (string-append "expected \\(Ccase-> \\(C→ Zero Zero\\) \\(C→ Int Int\\)\\), "
+                 "given \\(Ccase-> .*\\(C→ NegInt \\(U NegInt Zero\\)\\) .*\\(C→ Zero PosInt\\) "
+                 ".*\\(C→ PosInt PosInt\\) .*\\(C→ Nat PosInt\\) .*\\(C→ Int Int\\)\\)"))