In nested if, eq? breaks occurrence typing

The code below does not typecheck (and expands to such code):

(λ ([val : (U (List 'x 'y) (List 'z))])
  (if (if (pair? (cdr val))
          (eq? 'x (car val))
          #f)
      (ann val (List 'x 'y))
      (ann val (List 'z)))) ;; TR says val is (U (List 'x 'y) (List 'z)) here

If we wrap the (eq? 'x (car val)) with an (if … #t #f), it typechecks without problem:

(λ ([val : (U (List 'x 'y) (List 'z))])
  (if (if (pair? (cdr val))
          (if (eq? 'x (car val))
              #t
              #f)
          #f)
      (ann val (List 'x 'y))
      (ann val (List 'z)))) ;; Okay

This last example shows that wrapping the eq? with (if … #t #f) is not enough if the eq? further refines the type.

(λ ([val : (U (List 'x 'y) (List 'x 'w) (List 'z))])
  (if (if (eq? 'x (car val))
          (if (eq? 'y (cadr val)) #t #f)
          #f)
      (ann val (List 'x 'y))
      (ann val (U (List 'x 'w) (List 'z))))) ;; TR says val is (U (List x y) (List x w) (List z)) here

Start by running the three Typed Racket reproductions in the issue and compare occurrence-typing behavior for nested if expressions involving pair?, eq?, car, and cadr. Done means the examples typecheck while retaining the expected refined types in both branches.