diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
index be8c91e9a8..55d1527f0e 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
@@ -155,7 +155,7 @@
      [`(cross ,s)
       (lang-enum-get-cross-enum l-enum s)]
      [`(list ,sub-pats ...)
-      (list/e
+      (apply list/e
        (for/list ([sub-pat (in-list sub-pats)])
          (match sub-pat
            [`(repeat ,pat #f #f)
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt
index 3f9e5a1eca..ed30b5f1e3 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/enumerator.rkt
@@ -104,7 +104,7 @@
                (λ (n)
                   (encode e (inv-f n))))]
         [else
-         (define es/e (list/e (cons e es)))
+         (define es/e (apply list/e (cons e es)))
          (map/e
           (λ (xs)
              (apply f xs))
@@ -497,7 +497,7 @@
 ;; Traversal (maybe come up with a better name
 ;; traverse/e : (a -> enum b), (listof a) -> enum (listof b)
 (define (traverse/e f xs)
-  (list/e (map f xs)))
+  (apply list/e (map f xs)))
 
 ;; Hash Traversal
 ;; hash-traverse/e : (a -> enum b), (hash[k] -o> a) -> enum (hash[k] -o> b)
@@ -839,7 +839,7 @@
                (disj-sum/e (cons (const/e '()) null?)
                            (cons (cons/e e self) pair?))))]
     [(e n)
-     (list/e (build-list n (const e)))]))
+     (apply list/e (build-list n (const e)))]))
 
 ;; many1/e : enum a -> enum (nonempty listof a)
 (define (many1/e e)
@@ -917,25 +917,113 @@
   (loop xs -1 '()))
 
 ;; list/e : listof (enum any) -> enum (listof any)
-(define (list/e es)
+(define (list/e . es)
   (define l (length es))
   (cond
     [(= l 0) (const/e '())]
     [(= l 1) (map/e list car (car es))]
+    [(all-infinite? es) (apply box-list/e es)]
+    [(all-finite?   es) (apply nested-cons-list/e es)]
     [else
-     (define split-point (quotient l 2))
-     (define-values (left right) (split-at es split-point))
-     (map/e
-      (λ (pr) (append (car pr) (cdr pr)))
-      (λ (lst)
-        (define-values (left right) (split-at lst split-point))
-        (cons left right))
-      (cons/e (list/e left) (list/e right)))]))
+     (define tagged-es
+       (for/list ([i (in-naturals)]
+                  [e (in-list es)])
+         (cons e i)))
+     (define-values (inf-eis fin-eis)
+       (partition (compose infinite?
+                           size
+                           car)
+                  tagged-es))
+     (define inf-es (map car inf-eis))
+     (define inf-is (map cdr inf-eis))
+     (define fin-es (map car fin-eis))
+     (define fin-is (map cdr fin-eis))
+     
+     (define inf-slots
+       (reverse
+        (let loop ([inf-is inf-is]
+                   [fin-is fin-is]
+                   [acc    '()])
+          (match* (inf-is fin-is)
+            [('() '()) acc]
+            [((cons _ _) '())
+             (append (for/list ([_ (in-list inf-is)]) #t) acc)]
+            [('() (cons _ _))
+             (append (for/list ([_ (in-list fin-is)]) #f) acc)]
+            [((cons ii rest-iis) (cons fi rest-fis))
+             (cond [(ii . < . fi)
+                    (loop rest-iis
+                          fin-is
+                          (cons #t acc))]
+                   [else
+                    (loop inf-is
+                          rest-fis
+                          (cons #f acc))])]))))
+     
+     (define/match (reconstruct infs-fins)
+       [((cons infs fins))
+        (let loop ([infs infs]
+                    [fins fins]
+                    [inf?s inf-slots]
+                    [acc '()])
+           (match inf?s
+             ['() (reverse acc)]
+             [(cons inf? rest)
+              (cond [inf?
+                     (loop (cdr infs)
+                           fins
+                           rest
+                           (cons (car infs) acc))]
+                    [else
+                     (loop infs
+                           (cdr fins)
+                           rest
+                           (cons (car fins) acc))])]))])
+     (define (deconstruct xs)
+       (let loop ([xs xs]
+                  [inf-acc '()]
+                  [fin-acc '()]
+                  [inf?s   inf-slots])
+         (match* (xs inf?s)
+           [('() '()) (cons (reverse inf-acc)
+                            (reverse fin-acc))]
+           [((cons x rest-xs) (cons inf? rest-inf?s))
+            (cond [inf?
+                   (loop rest-xs
+                         (cons x inf-acc)
+                         fin-acc
+                         rest-inf?s)]
+                  [else
+                   (loop rest-xs
+                         inf-acc
+                         (cons x fin-acc)
+                         rest-inf?s)])])))
+     (map/e reconstruct
+            deconstruct
+            (cons/e (apply list/e inf-es)
+                    (apply list/e fin-es)))]))
 
-(define/contract (all-infinite? es)
-  ((listof enum?) . -> . boolean?)
+(define (nested-cons-list/e . es)
+  (define l (length es))
+  (define split-point (quotient l 2))
+  (define-values (left right) (split-at es split-point))
+  (map/e
+   (λ (pr) (append (car pr) (cdr pr)))
+   (λ (lst)
+      (define-values (left right) (split-at lst split-point))
+      (cons left right))
+   (cons/e (apply list/e left) (apply list/e right))))
+
+
+(define (all-infinite? es)
+  (all-sizes-something? infinite? es))
+
+(define (all-finite? es)
+  (all-sizes-something? (negate infinite?) es))
+
+(define (all-sizes-something? p? es)
   (for/and ([e (in-list es)])
-    (infinite? (size e))))
+    (p? (size e))))
 
 ;; Fair tupling via generalized cantor n-tupling
 ;; ordering is monotonic in the sum of the elements of the list
@@ -943,8 +1031,7 @@
   (define all-inf? (all-infinite? es))
   (cond [(empty? es) (const/e '())]
         [(not all-inf?)
-         ;; TODO: improve mixed finite/infinite
-         (list/e es)]
+         (apply list/e es)]
         [else
          (define k (length es))
          (define dec
@@ -962,7 +1049,7 @@
 (define (box-list/e . es)
   (define all-inf? (all-infinite? es))
   (cond [(empty? es) (const/e '())]
-        [(not all-inf?) (list/e es)]
+        [(not all-inf?) (apply list/e es)]
         [else
          (define k (length es))
          (define dec
@@ -988,7 +1075,7 @@
          (map/e
           (curry cons bound)
           cdr
-          (list/e
+          (apply list/e
            (for/list ([_ (in-range (sub1 len))])
              bounded/e))))
        (define first-not-max/e
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/enum-examples.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/enum-examples.rkt
deleted file mode 100644
index a17837c2ff..0000000000
--- a/pkgs/redex-pkgs/redex-test/redex/tests/enum-examples.rkt
+++ /dev/null
@@ -1,243 +0,0 @@
-#lang racket/base
-(require rackunit
-         redex/reduction-semantics)
-
-(define-language Base
-  (x a b c)
-  (y d e f))
-
-;; Simple repeats
-(define-extended-language S1 Base
-  (s (x ... y ...)))
-
-#;
-(append/e (many/e (enum x))
-          (many/e (enum y)))
-
-(define-extended-language S2 Base
-  (s (x ..._1 y ..._1)))
-
-#;
-(dep/e nats
-       (λ (len)
-          (append/e (listof n (enum x))
-                    (listof n (enum y)))))
-
-(define-extended-language S3 Base
-  (s (x_1 ..._1 x_1 ..._1)))
-
-#;
-(dep/e nats
-       (λ (len)
-          (dep/e (listof n (enum x))
-                 (λ (x-vals)
-                    (append/e x-vals
-                              x-vals)))))
-
-;; Nesting!
-(define-extended-language S4 Base
-  (s ((x ...) ... (y ...) ...)))
-
-#;
-(append/e (many/e (append/e (many/e (enum x))))
-          (many/e (append/e (many/e (enum y)))))
-
-(define-extended-language S5 Base
-  (s ((x ...) ..._1 (y ...) ..._1)))
-
-#;
-(dep/e nats
-       (λ (len)
-          (append/e (listof n (append/e (many (enum x))))
-                    (listof n (append/e (many (enum y)))))))
-
-(define-extended-language S6 Base
-  (s ((x ..._1) ..._2 (y ..._1) ..._2)))
-
-
-;; mapM/e : (a -> enum b) -> [a] -> ([a] -> enum [b])
-;; (compose mapM/e mapM/e) : (a -> enum b) -> [[a]] -> ([[a]] -> enum [[b]])
-;; 
-#;
-(dep/e nats
-       (λ (len2)
-          (dep/e (listof nats)
-                 (λ (len1s)
-                    (append/e (listof len2
-                                      (mapM/e (λ (len1)
-                                                 (listof len1 (enum x)))
-                                              len1s))
-                              (listof len2
-                                      (mapM/e (λ (len1)
-                                                 (listof len1 (enum y)))
-                                              len1s)))))) )
-
-;; 
-(define-extended-language S7 Base
-  (s ((x_1 ..._1) ..._2 (x_1 ..._1) ..._2)))
-
-
-#;
-(dep/e nats
-       (λ (len2)
-          (dep/e (listof nats)
-                 (λ (len1s)
-                    (dep/e
-                     ;; We need to enumerate them in the context of the outermost "rigid"/named pattern
-                     (listof len2
-                             (mapM/e (λ (len1)
-                                        (listof len1 (enum x))))) ;; this is an important part!!!!
-                     ;; [[x]]
-                     ;; we're lucky that they're the same this time, what if it's more complicated though?
-                     (λ (xss)
-                        (append/e xss
-                                  xss)))))))
-
-;; This one has different underlying patterns
-(define-extended-language S8 Base
-  (s (((x_1 y) ..._1) ..._2
-      (x_1     ..._1) ..._2)))
-
-#;
-(dep/e nats
-       (λ (len2)
-          (dep/e (listof nats)
-                 (λ (len1s)
-                    (dep/e
-                     ;; We need to enumerate them in the context of the outermost "rigid"/named pattern
-                     (listof len2
-                             (mapM/e (λ (len1)
-                                        (listof len1 (enum x))))) ;; this is an important part!!!!
-                     ;; [[x]]
-                     (λ (xss)
-                        (append/e ((compose  mapM/e  mapM/e)
-                                   (λ (x)
-                                      (map/e (λ (y)
-                                                (cons x y))
-                                             (enum y)))
-                                   (xss))
-                                  ((compose mapM/e mapM/e)
-                                   (λ (x)
-                                      (const/enum x))
-                                   xss))))))))
-
-
-;; This one has different patterns that differ at a higher branch
-(define-extended-language S9 Base
-  (s ((x_1 ..._1 y) ..._2
-      (x_1 ..._1)   ..._2)))
-
-#;
-(dep/e nats
-       (λ (len2)
-          (dep/e  (listof len2 nats)
-                  (λ (len1s)
-                     (dep/e
-                      (listof len2
-                              (mapM/e (λ (len1)
-                                         (listof len1 (enum x)))
-                                      len1s))
-                      (λ (x1ss)
-                         (append/e
-                          (mapM/e
-                           (λ (x1s)
-                              (append/e (mapM/e const x1s)
-                                        (singleton/e 1 (enum y)))))
-                          ((compose mapM/e mapM/e)
-                           const/e
-                           x1ss))))))))
-
-
-;; Next lets make the insides even more compilcated
-(define-extended-language S10 Base
-  (s (((y_2
-        (x_1 y)              ..._1
-        y ...)     ..._2
-       y ...
-       (y
-        (x_1 (x_1 x_1))      ..._1
-        y_2)       ..._2)
-       y ...
-       y)))
-
-#;
-;; This one's a doozy so hopefully it will be similar to the general construction
-(dep/e (vals/e ((iterate 0) nats))
-       (λ (len2)
-          ;; as long as multiple parts of the list need access to the
-          ;; same vars you need to keep everyone within the dep/e
-          
-          ;; as you descend deeper you need to do that many listofs
-          ;; when you enumerate so in the algorithm you'll need to
-          ;; keep track of that.
-          
-          ;; you also must enumerate all variables that are at that
-          ;; depth, in this way named vals and named repeats are similar
-          (dep/e (vals/e ((iterate 1 (curry many/e
-                                            len2)) nats)
-                         ((iterate 1 (curry many/e
-                                            len2)) (enum y)))
-                 (λ (len1s ys)
-                    (dep/e
-                     (vals/e (((iterate 0 mapM/e)
-                               (λ (len2)
-                                  ((iterate 1 mapM/e)
-                                   (λ (len1)
-                                      (listof len1 (enum x))))
-                                  len1s))
-                              len2))
-
-                     ;; 2 levels deep
-                     (λ (xss)
-                        (append/e
-                         ;;
-                         ((iterate 0 mapM/e)
-                          (λ (len2)
-                             ((iterate 1 mapM/e)
-                              (λ (len1 y xs)
-                                 (append/e
-                                  (singleton/e (const/e y))
-                                  (mapM/e (λ (x)
-                                             (list/e (const/e x)
-                                                     (enum y)))
-                                          xs)
-                                  (many y)))
-                              ys
-                              xss))
-                          len2)
-                         (many (enum y))
-                         ;; The complications of the above iterate
-                         ;; mapM/e's might not be necessary so I'm not using them here
-                         (mapM/e
-                          (λ (y xs)
-                             (append/e
-                              (singleton/e (enum y))
-                              (mapM/e
-                               (λ (x)
-                                  (list/e (const/e x)
-                                          (list/e x x)))
-                               xs)
-                              (mapM/e
-                               const/e
-                               ys)))
-                          ys
-                          xss)
-                         (many (enum y))
-                         (singleton/e (enum y)))))))))
-
-
-;; Then have them be 3 wide instead of 2
-#;
-(define-extended-language S11 Base
-  (s ((x_1 ..._1 y) ..._2
-      (x_1 ..._1)   ..._2)))
-
-;; We should also do 3 deep  
-
-  #;
-
-  
-;; Nesting something within itself, yikes!
-(define-extended-language S12 Base
-  (s ((x_1 ..._1 y) ..._2
-      (x_1 ..._1)   ..._2)))
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt
index cc9ea1e802..1634a1ff87 100644
--- a/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt
+++ b/pkgs/redex-pkgs/redex-test/redex/tests/enumerator-test.rkt
@@ -323,6 +323,12 @@
  (check-equal? (list->inc-set '(2 0 1 2)) '(2 3 5 8))
  (check-equal? (inc-set->list '(2 3 5 8)) '(2 0 1 2)))
 
+;; mixed finite/infinite list/e tests
+(test-begin
+ (check-bijection? (list/e bool/e (cons/e bool/e bool/e) (fin/e 'foo 'bar 'baz)))
+ (check-bijection? (list/e nats/e string/e (many/e bool/e)))
+ (check-bijection? (list/e bool/e nats/e ints/e string/e (cons/e bool/e bool/e))))
+
 ;; multi-arg map/e test
 (define sums/e
   (map/e