diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt
index df4b2b4503..6eadfa91f1 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt
@@ -27,15 +27,25 @@
 (define-judgment-form STLC
   #:mode (typeof I I O)
   #:contract (typeof Γ e τ)
-  [(typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))
-   (typeof ([x τ_1] Γ) e τ_2)]
-  [(typeof Γ (e_1 e_2) τ)
-   (typeof Γ e_1 (τ_2 → τ))
-   (typeof Γ e_2 τ_2)]
-  [(typeof Γ x τ)
-   (where τ (lookup Γ x))]
-  [(typeof Γ i int)]
-  [(typeof Γ add1 (int → int))])
+  
+  [(typeof ([x τ_1] Γ) e τ_2)
+   ------------------------------------
+   (typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))]
+  
+  [(typeof Γ e_1 (τ_2 → τ))
+   (typeof Γ e_2 τ_2)
+   ------------------------
+   (typeof Γ (e_1 e_2) τ)]
+  
+  [(where τ (lookup Γ x))
+   --------------
+   (typeof Γ x τ)]
+  
+  [----------------
+   (typeof Γ i int)]
+  
+  [---------------------------
+   (typeof Γ add1 (int → int))])
 
 
 (define-metafunction STLC
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules.rkt
index 857ec56070..58eacd2d9a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/define-judgment-form/typing-rules.rkt
@@ -35,15 +35,25 @@
 (define-judgment-form STLC
   #:mode (typeof I I O)
   #:contract (typeof Γ e τ)
-  [(typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))
-   (typeof (extend Γ x τ_1) e τ_2)]
-  [(typeof Γ (e_1 e_2) τ)
-   (typeof Γ e_1 (τ_2 → τ))
-   (typeof Γ e_2 τ_2)]
-  [(typeof Γ x τ)
-   (where τ (lookup Γ x))]
-  [(typeof Γ i int)]
-  [(typeof Γ add1 (int → int))])
+  
+  [(typeof (extend Γ x τ_1) e τ_2)
+   ------------------------------------
+   (typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))]
+  
+  [(typeof Γ e_1 (τ_2 → τ))
+   (typeof Γ e_2 τ_2)
+   ------------------------
+   (typeof Γ (e_1 e_2) τ)]
+  
+  [(where τ (lookup Γ x))
+   --------------
+   (typeof Γ x τ)]
+  
+  [----------------
+   (typeof Γ i int)]
+  
+  [----------------------------
+   (typeof Γ add1 (int → int))])
 
 (define-metafunction STLC
   extend : Γ x τ -> Γ