test.rkt

#lang racket/base

(require
 redex/reduction-semantics)

(define-language lc
  [e m ::= natural x (λ (x) e) (e e)]
  [x ::= variable-not-otherwise-mentioned]
  #:binding-forms
  (λ (x) e #:refers-to x))

(define lc-->
  (reduction-relation
   lc
   (--> ((λ (x) e) m) (substitute e x m))))

(module+ test
  (test-->> (compatible-closure lc--> lc e)
    (term (λ (x) ((λ (y) y) 1)))
    (term (λ (x) 1)))
  (test-->> (compatible-closure lc--> lc m)
    (term (λ (x) ((λ (y) y) 1)))
    (term (λ (x) 1))))

Well, this has made it clear to me that the way Redex is implementing these "alias" non-terminals is just wrong. Thanks for helping me figure that out!