diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
index 9e728b23..657be1e3 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -45,24 +45,11 @@
        ;; objects yet.
        (let-values
            ([(o-a t-a) (for/lists (os ts)
-                         ([nm (in-range dom-count)]
+                         ([_ (in-range dom-count)]
                           [oa (in-sequence-forever (in-list o-a) -empty-obj)]
-                          [ta (in-sequence-forever (in-list t-a) #f)])
+                          [ta (in-sequence-forever (in-list t-a) Univ)])
                          (values oa ta))])
-           (match rng
-            [(AnyValues: f) (tc-any-results f)]
-            [(Values: results)
-             (define-values (t-r f-r o-r)
-               (for/lists (t-r f-r o-r)
-                 ([r (in-list results)])
-                 (open-Result r o-a t-a)))
-             (ret t-r f-r o-r)]
-            [(ValuesDots: results dty dbound)
-             (define-values (t-r f-r o-r)
-               (for/lists (t-r f-r o-r)
-                 ([r (in-list results)])
-                 (open-Result r o-a t-a)))
-             (ret t-r f-r o-r dty dbound)])))]
+           (open-Values rng o-a t-a)))]
     ;; this case should only match if the function type has mandatory keywords
     ;; but no keywords were provided in the application
     [((arr: _ _ _ _
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
index 7b23bac7..455871c2 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
@@ -9,11 +9,30 @@
          (except-in (types abbrev utils filter-ops) -> ->* one-of/c)
          (rep type-rep object-rep filter-rep rep-utils))
 
-(provide open-Result add-scope values->tc-results)
+(provide add-scope values->tc-results)
 
 (provide/cond-contract
+  [open-Values (-> SomeValues/c (listof Object?) (listof Type/c) -> full-tc-results/c)]
   [replace-names (-> (listof (list/c identifier? Object?)) tc-results/c tc-results/c)])
 
+(define (open-Values v os ts)
+  (match v
+    [(AnyValues: f)
+     (tc-any-results f)]
+    [(Values: results)
+     (define-values (t-r f-r o-r)
+       (for/lists (t-r f-r o-r)
+         ([r (in-list results)])
+         (open-Result r os ts)))
+     (ret t-r f-r o-r)]
+    [(ValuesDots: results dty dbound)
+     (define-values (t-r f-r o-r)
+       (for/lists (t-r f-r o-r)
+         ([r (in-list results)])
+         (open-Result r os ts)))
+     (ret t-r f-r o-r dty dbound)]))
+
+
 ;; Substitutes the given objects into the type, filters, and object
 ;; of a Result for function application. This matches up to the substitutions
 ;; in the T-App rule from the ICFP paper.