diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
index f9e10f5d93..b9197822bd 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
@@ -1,18 +1,8 @@
-3,4d2
+3c3
 < (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
+---
 > (define the-error "swaps to/from expressions when recurring in the rhs of app")
-> 
-113a114,115
->   [(subst (M N) x M_x)
->    ((subst M_x x M) (subst N x M_x))]
-118,119d119
-<   [(subst (M N) x M_x)
+119c119
 <    ((subst M x M_x) (subst N x M_x))]
-257a258
-> 
+---
+>    ((subst M_x x M) (subst N x M_x))]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
index 2584a83df9..1d62818511 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
@@ -1,15 +1,15 @@
 #lang racket/base
 
+(define the-error "swaps to/from expressions when recurring in the rhs of app")
+
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          math/base)
 
 (provide (all-defined-out))
-(define the-error "swaps to/from expressions when recurring in the rhs of app")
-
 
 (define-language stlc
   (M N ::= 
@@ -111,12 +111,12 @@
    (λ (x τ) M)]
   [(subst (λ (x_1 τ) M) x_2 v)
    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-  [(subst (M N) x M_x)
-   ((subst M_x x M) (subst N x M_x))]
    (where x_new ,(variable-not-in (term (x_1 e x_2))
                                   (term x_1)))]
   [(subst (c M) x M_x)
    (c (subst M x M_x))]
+  [(subst (M N) x M_x)
+   ((subst M_x x M) (subst N x M_x))]
   [(subst M x M_x)
    M])
 
@@ -255,7 +255,6 @@
        (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
   (match candidate
     [`(typeof • ,M ,τ)
-
      M]
     [#f #f]))