`redex-check` doesn't warn about ellipsis in judgment-forms more than one level deep

#lang racket
(require redex/reduction-semantics)

(define-language simple-plus
  (M (e e))
  (e natural))

(define-judgment-form simple-plus
  #:mode (okay1 I I)
  [
   --------
   (okay1 M (e ...))])

(define-judgment-form simple-plus
  #:mode (okay I)
  [(okay1 M ())
   --------
   (okay M)])

(redex-check simple-plus
 #:satisfying (okay e)
 (term e))

simply fails to generate terms. Note that if the okay in the redex-check is replaced with okay1 or if e is changes to have an ellipsis (ie changing e to (e ::= natural (+ e ...))) one gets the error (#:satisfying keyword does not support ellipses, contexts, side-conditions, or unquote)

Start by running the provided reproducer and tracing the redex-check entry point, especially how #:satisfying processes the okay judgment form and nested ellipses in define-judgment-form. Compare it with the okay1 and altered-language cases described in the issue. Done means the nested case reports the appropriate unsupported construct instead of silently failing to generate terms.