diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt
index 154f5cd..ce56846 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt
@@ -1,6 +1,5 @@
 #lang s-exp "../../rosette/rosette2.rkt"
-(require "../rackunit-typechecking.rkt"
-         "check-type+asserts.rkt")
+(require "../rackunit-typechecking.rkt")
 
 ;; Examples from the Rosette Guide, Section 4.4
 
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec45-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec45-tests.rkt
new file mode 100644
index 0000000..7bead9f
--- /dev/null
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec45-tests.rkt
@@ -0,0 +1,21 @@
+#lang s-exp "../../rosette/rosette2.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; Examples from the Rosette Guide, Section 4.5
+
+;; 4.5 Procedures
+(define-symbolic b boolean?)
+(define-symbolic x integer?)
+(define p (if b * -)) ; p is a symbolic procedure
+(check-type p : (→ Num Num Num))
+(check-not-type p : (C→ Num Num Num)) ; should not have concrete type
+(check-type p : (→ Int Int Int))
+(define sol (synthesize #:forall (list x)
+                        #:guarantee (assert (= x (p x 1)))))
+(check-type (evaluate p sol) : (→ Int Int Int) -> *)
+;; this doesnt hold bc type of result is from p
+;(check-type (evaluate p sol) : (→ PosInt PosInt PosInt) -> *)
+(define sol2 (synthesize #:forall (list x)
+                        #:guarantee (assert (= x (p x 0)))))
+(check-type (evaluate p sol2) : (→ Int Int Int) -> -)
+(check-not-type (evaluate p sol2) : (→ PosInt PosInt PosInt))