diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
index 68b32b3..4866db8 100644
--- a/tapl/stlc+sub.rkt
+++ b/tapl/stlc+sub.rkt
@@ -1,5 +1,6 @@
 #lang s-exp "typecheck.rkt"
 (extends "stlc+lit.rkt" #:except #%datum +)
+(reuse add1 #:from "ext-stlc.rkt")
 (provide (for-syntax subs? current-sub?))
 
 ;; Simply-Typed Lambda Calculus, plus subtyping
diff --git a/tapl/tests/stlc+sub-tests.rkt b/tapl/tests/stlc+sub-tests.rkt
index 4ecbf4a..6ff29dd 100644
--- a/tapl/tests/stlc+sub-tests.rkt
+++ b/tapl/tests/stlc+sub-tests.rkt
@@ -21,6 +21,12 @@
 (check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
 (check-not-type (λ ([x : Int]) x) : (→ Num Int))
 
+(check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0)
+(check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2)
+(typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1))
+(check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2)
+(typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1))
+
 (check-type + : (→ Num Num Num))
 (check-type + : (→ Int Num Num))
 (check-type + : (→ Int Int Num))