diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index b01e14cd..4f6283c7 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -1,7 +1,7 @@
 #lang racket/base
 
 (require (rename-in "../utils/utils.rkt" [infer infer-in]))
-(require racket/match
+(require racket/match racket/list
          (only-in unstable/list list-update)
          (for-syntax racket/base syntax/parse)
          (contract-req)
@@ -62,19 +62,22 @@
 
 ;; Returns #f if anything becomes (U)
 (define (env+ env fs)
-  (let/ec exit
+  (let/ec exit*
+    (define (exit) (exit* #f empty))
     (define-values (props atoms) (combine-props fs (env-props env) exit))
-    (for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)])
-      (match f
-        [(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x)))
-         (update-type/lexical
-           (lambda (x t)
-             (define new-t (update t ft (TypeFilter? f) lo))
-             (when (type-equal? new-t -Bottom)
-               (exit #f))
-             new-t)
-           x Γ)]
-        [_ Γ]))))
+    (values
+      (for/fold ([Γ (replace-props env props)]) ([f (in-list atoms)])
+        (match f
+          [(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x)))
+           (update-type/lexical
+             (lambda (x t)
+               (define new-t (update t ft (TypeFilter? f) lo))
+               (when (type-equal? new-t -Bottom)
+                 (exit))
+               new-t)
+             x Γ)]
+          [_ Γ]))
+      atoms)))
 
 ;; run code in an extended env and with replaced props. Requires the body to return a tc-results.
 ;; TODO make this only add the new prop instead of the entire environment once tc-id is fixed to
@@ -85,10 +88,10 @@
     (pattern (~seq) #:with form #'(begin)))
   (syntax-parse stx
     [(_ ps:expr u:unreachable? . b)
-     #'(let ([new-env (env+ (lexical-env) ps)])
+     #'(let-values ([(new-env atoms) (env+ (lexical-env) ps)])
          (if new-env
              (with-lexical-env new-env
-               (add-unconditional-prop (let () . b) (apply -and (env-props new-env))))
+               (add-unconditional-prop (let () . b) (apply -and (append atoms (env-props new-env)))))
              (let ()
                u.form
                (ret -Bottom))))]))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
index 2183e061..3ad139b9 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
@@ -59,7 +59,7 @@
       [(cons p ps) (cons p (loop ps))])))
 
 (define/cond-contract (combine-props new-props old-props exit)
-  ((listof Filter/c) (listof Filter/c) (-> #f none/c)
+  ((listof Filter/c) (listof Filter/c) (-> none/c)
    . -> .
    (values (listof (or/c ImpFilter? OrFilter?)) (listof (or/c TypeFilter? NotTypeFilter?))))
   (define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p)))
@@ -96,7 +96,7 @@
 
             [(AndFilter: ps) (loop derived-formulas derived-atoms (append ps (cdr worklist)))]
             [(Top:) (loop derived-formulas derived-atoms (cdr worklist))]
-            [(Bot:) (exit #f)])))))
+            [(Bot:) (exit)])))))
 
 
 (define (unconditional-prop res)