diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff
index 420e3cde88..24394476e0 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff
@@ -6,7 +6,7 @@
 <    (tc-down (x y Γ) M (λ y κ) σ_ans)
 ---
 >    (tc-down (x y Γ) M (λ x κ) σ_ans)
-571a572,574
+552a553,555
 > 
 > (define small-counter-example '(hd ((λ x x) 1)))
 > (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff
index be23186576..0fad0aa17b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff
@@ -16,7 +16,7 @@
 <   [(where #t (not-v? M))
 <    (tc-down Γ ((λ x N) M) κ σ_2)
 <    ---------------------------------
-571a567,572
+552a548,553
 > 
 > (define small-counter-example '(let ([x (new nil)])
 >                                  ((λ ignore
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff
index 41410541d9..927078a0f3 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff
@@ -6,7 +6,7 @@
 <    (where G (unify τ_2 (τ_1 → x)))
 ---
 >    (where G (unify τ_1 (τ_2 → x)))
-571a572,574
+552a553,555
 > 
 > (define small-counter-example (term (1 cons)))
 > (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
index 745e3ef770..61968e952e 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
@@ -4,11 +4,11 @@
 > (define the-error
 >   (string-append "misspelled the name of a metafunction in a side-condition, "
 >                  "causing the occurs check to not happen"))
-212c214
-<   [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+205c207
+<   [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
 ---
->   [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))]
-571a574,576
+>   [(uh (x τ G) Gx) ⊥ (where #t (in-vars? x τ))]
+552a555,557
 > 
 > (define small-counter-example (term ((λ x (x x)) hd)))
 > (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff
index 9fb29dc23d..8f7fafb83a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff
@@ -2,7 +2,7 @@
 < (define the-error "no error")
 ---
 > (define the-error "eliminate-G was written as if it always gets a Gx as input")
-225,226c225,228
+214,215c214,217
 <   [(eliminate-G x τ (σ_1 σ_2 G))
 <    ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
 ---
@@ -10,7 +10,7 @@
 >    (τ (eliminate-τ x τ σ) (eliminate-G x τ G))]
 >   [(eliminate-G x τ (y σ G))
 >    (y (eliminate-τ x τ σ) (eliminate-G x τ G))])
-560,571c562,577
+541,552c543,558
 <       (let ([t-type (type-check M)])
 <         (implies
 <          t-type
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff
index 51deff07c3..4416f384db 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff
@@ -2,11 +2,11 @@
 < (define the-error "no error")
 ---
 > (define the-error "∨ has an incorrect duplicated variable, leading to an uncovered case")
-240c240
+229c229
 <   [(∨ boolean_1 boolean_2) #t])
 ---
 >   [(∨ boolean boolean) #t])
-560,571c560,575
+541,552c541,556
 <       (let ([t-type (type-check M)])
 <         (implies
 <          t-type
@@ -34,5 +34,5 @@
 >                                (or (equal? red-t "error")
 >                                    (zero? n) (loop red-t (- n 1))))))))))))))
 > 
-> (define small-counter-example (term ((λ x x) 1)))
+> (define small-counter-example (term (λ x (x x))))
 > (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff
index 31dcf22a1b..4bcfdf055d 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff
@@ -9,13 +9,13 @@
 <      (let ([x E]) M))
 ---
 >      (v E))
-306,307c307,308
+287,288c288,289
 <    (--> (Σ (in-hole E (let ([x v]) M)))
 <         (Σ (in-hole E (subst M x v)))
 ---
 >    (--> (Σ (in-hole E (let ([x M]) N)))
 >         (Σ (in-hole E ((λ x N) M)))
-571a573,575
+552a554,556
 > 
 > (define small-counter-example (term (let ((x (λ y y))) (x x))))
 > (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt
index 94c907bef5..b7f2afabb3 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt
@@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
 
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
-  [(unify τ σ) (uh (τ σ ·) · #f)])
+  [(unify τ σ) (uh (τ σ ·) ·)])
 
 #|
 
-Algorithm copied from _An Efficient Unification Algorithm_ by 
-Alberto Martelli and Ugo Montanari (section 2).
-http://www.nsl.com/misc/papers/martelli-montanari.pdf
-
-This isn't the eponymous algorithm; it is an earlier one
-in the paper that's simpler.
+Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
+Unification Theory by Franz Baader and Wayne Synder
+http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
 
 The 'uh' function iterates over a set of equations applying the
-rules from the paper, moving them from the first argument to
-the second argument and tracking when something changes.
-It runs until there are no more changes. The (a), (b),
-(c), and (d) are the rule labels from the paper.
+rules from the paper, building up the result substitution in G_r.
 
 |#
 
 (define-metafunction stlc
-  uh : G G boolean -> Gx or ⊥
-
-  [(uh · G #t) (uh G · #f)]
-  [(uh · G #f) G]
+  uh : G Gx -> Gx or ⊥
   
-  ;; (a)
-  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  [(uh · Gx) Gx]
   
-  ;; (b)
-  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  ;; orient
+  [(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
   
-  ;; (c) -- term reduction
-  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
-  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  ;; trivial (other cases are covered by decomposition rule)
+  [(uh (x x G) Gx) (uh G Gx)]
   
-  ;; (c) -- failure
-  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  ;; decomposition
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
+  [(uh ((list τ)    (list σ)    G) Gx) (uh (τ σ G)               Gx)]
+  [(uh ((ref τ)     (ref σ)     G) Gx) (uh (τ σ G)               Gx)]
+  [(uh (int         int         G) Gx) (uh G                     Gx)]
   
-  ;; (d) -- x occurs in τ case
-  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  ;; symbol clash
+  [(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
-  ;; (d) -- x does not occur in τ case
-  [(uh (x τ G) G_r boolean)
-   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
-   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  ;; occurs check
+  [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
   
-  ;; no rules applied; try next equation, if any.
-  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+  ;; variable elimination
+  [(uh (x τ G) Gx)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
 
 (define-metafunction stlc
   eliminate-G : x τ G -> G
@@ -253,14 +242,6 @@ It runs until there are no more changes. The (a), (b),
   [(in-vars-τ? x x) #t]
   [(in-vars-τ? x y) #f])
 
-(define-metafunction stlc
-  in-vars-G? : x G -> boolean
-  [(in-vars-G? x ·) #f]
-  [(in-vars-G? x (x τ G)) #t]
-  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
-                             (∨ (in-vars-τ? x τ)
-                                (in-vars-G? x G)))])
-
 (define-metafunction stlc
   apply-subst-τ : Gx τ -> τ
   [(apply-subst-τ · τ) τ]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt
index 5bfd58a2fc..4683930a75 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt
@@ -163,56 +163,45 @@ bring that type back, recurring on the continuation.
 
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
-  [(unify τ σ) (uh (τ σ ·) · #f)])
+  [(unify τ σ) (uh (τ σ ·) ·)])
 
 #|
 
-Algorithm copied from _An Efficient Unification Algorithm_ by 
-Alberto Martelli and Ugo Montanari (section 2).
-http://www.nsl.com/misc/papers/martelli-montanari.pdf
-
-This isn't the eponymous algorithm; it is an earlier one
-in the paper that's simpler.
+Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
+Unification Theory by Franz Baader and Wayne Synder
+http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
 
 The 'uh' function iterates over a set of equations applying the
-rules from the paper, moving them from the first argument to
-the second argument and tracking when something changes.
-It runs until there are no more changes. The (a), (b),
-(c), and (d) are the rule labels from the paper.
+rules from the paper, building up the result substitution in G_r.
 
 |#
 
 (define-metafunction stlc
-  uh : G G boolean -> Gx or ⊥
-
-  [(uh · G #t) (uh G · #f)]
-  [(uh · G #f) G]
+  uh : G Gx -> Gx or ⊥
   
-  ;; (a)
-  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  [(uh · Gx) Gx]
   
-  ;; (b)
-  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  ;; orient
+  [(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
   
-  ;; (c) -- term reduction
-  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
-  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  ;; trivial (other cases are covered by decomposition rule)
+  [(uh (x x G) Gx) (uh G Gx)]
   
-  ;; (c) -- failure
-  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  ;; decomposition
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
+  [(uh ((list τ)    (list σ)    G) Gx) (uh (τ σ G)               Gx)]
+  [(uh ((ref τ)     (ref σ)     G) Gx) (uh (τ σ G)               Gx)]
+  [(uh (int         int         G) Gx) (uh G                     Gx)]
   
-  ;; (d) -- x occurs in τ case
-  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  ;; symbol clash
+  [(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
-  ;; (d) -- x does not occur in τ case
-  [(uh (x τ G) G_r boolean)
-   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
-   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  ;; occurs check
+  [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
   
-  ;; no rules applied; try next equation, if any.
-  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+  ;; variable elimination
+  [(uh (x τ G) Gx)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
 
 (define-metafunction stlc
   eliminate-G : x τ G -> G
@@ -248,14 +237,6 @@ It runs until there are no more changes. The (a), (b),
   [(in-vars-τ? x x) #t]
   [(in-vars-τ? x y) #f])
 
-(define-metafunction stlc
-  in-vars-G? : x G -> boolean
-  [(in-vars-G? x ·) #f]
-  [(in-vars-G? x (x τ G)) #t]
-  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
-                             (∨ (in-vars-τ? x τ)
-                                (in-vars-G? x G)))])
-
 (define-metafunction stlc
   apply-subst-τ : Gx τ -> τ
   [(apply-subst-τ · τ) τ]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt
index 79b4465f87..721d20ee72 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt
@@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
 
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
-  [(unify τ σ) (uh (τ σ ·) · #f)])
+  [(unify τ σ) (uh (τ σ ·) ·)])
 
 #|
 
-Algorithm copied from _An Efficient Unification Algorithm_ by 
-Alberto Martelli and Ugo Montanari (section 2).
-http://www.nsl.com/misc/papers/martelli-montanari.pdf
-
-This isn't the eponymous algorithm; it is an earlier one
-in the paper that's simpler.
+Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
+Unification Theory by Franz Baader and Wayne Synder
+http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
 
 The 'uh' function iterates over a set of equations applying the
-rules from the paper, moving them from the first argument to
-the second argument and tracking when something changes.
-It runs until there are no more changes. The (a), (b),
-(c), and (d) are the rule labels from the paper.
+rules from the paper, building up the result substitution in G_r.
 
 |#
 
 (define-metafunction stlc
-  uh : G G boolean -> Gx or ⊥
-
-  [(uh · G #t) (uh G · #f)]
-  [(uh · G #f) G]
+  uh : G Gx -> Gx or ⊥
   
-  ;; (a)
-  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  [(uh · Gx) Gx]
   
-  ;; (b)
-  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  ;; orient
+  [(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
   
-  ;; (c) -- term reduction
-  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
-  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  ;; trivial (other cases are covered by decomposition rule)
+  [(uh (x x G) Gx) (uh G Gx)]
   
-  ;; (c) -- failure
-  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  ;; decomposition
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
+  [(uh ((list τ)    (list σ)    G) Gx) (uh (τ σ G)               Gx)]
+  [(uh ((ref τ)     (ref σ)     G) Gx) (uh (τ σ G)               Gx)]
+  [(uh (int         int         G) Gx) (uh G                     Gx)]
   
-  ;; (d) -- x occurs in τ case
-  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  ;; symbol clash
+  [(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
-  ;; (d) -- x does not occur in τ case
-  [(uh (x τ G) G_r boolean)
-   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
-   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  ;; occurs check
+  [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
   
-  ;; no rules applied; try next equation, if any.
-  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+  ;; variable elimination
+  [(uh (x τ G) Gx)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
 
 (define-metafunction stlc
   eliminate-G : x τ G -> G
@@ -253,14 +242,6 @@ It runs until there are no more changes. The (a), (b),
   [(in-vars-τ? x x) #t]
   [(in-vars-τ? x y) #f])
 
-(define-metafunction stlc
-  in-vars-G? : x G -> boolean
-  [(in-vars-G? x ·) #f]
-  [(in-vars-G? x (x τ G)) #t]
-  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
-                             (∨ (in-vars-τ? x τ)
-                                (in-vars-G? x G)))])
-
 (define-metafunction stlc
   apply-subst-τ : Gx τ -> τ
   [(apply-subst-τ · τ) τ]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
index 7f1c1e32fd..df0045c7e2 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
@@ -170,56 +170,45 @@ bring that type back, recurring on the continuation.
 
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
-  [(unify τ σ) (uh (τ σ ·) · #f)])
+  [(unify τ σ) (uh (τ σ ·) ·)])
 
 #|
 
-Algorithm copied from _An Efficient Unification Algorithm_ by 
-Alberto Martelli and Ugo Montanari (section 2).
-http://www.nsl.com/misc/papers/martelli-montanari.pdf
-
-This isn't the eponymous algorithm; it is an earlier one
-in the paper that's simpler.
+Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
+Unification Theory by Franz Baader and Wayne Synder
+http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
 
 The 'uh' function iterates over a set of equations applying the
-rules from the paper, moving them from the first argument to
-the second argument and tracking when something changes.
-It runs until there are no more changes. The (a), (b),
-(c), and (d) are the rule labels from the paper.
+rules from the paper, building up the result substitution in G_r.
 
 |#
 
 (define-metafunction stlc
-  uh : G G boolean -> Gx or ⊥
-
-  [(uh · G #t) (uh G · #f)]
-  [(uh · G #f) G]
+  uh : G Gx -> Gx or ⊥
   
-  ;; (a)
-  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  [(uh · Gx) Gx]
   
-  ;; (b)
-  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  ;; orient
+  [(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
   
-  ;; (c) -- term reduction
-  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
-  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  ;; trivial (other cases are covered by decomposition rule)
+  [(uh (x x G) Gx) (uh G Gx)]
   
-  ;; (c) -- failure
-  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  ;; decomposition
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
+  [(uh ((list τ)    (list σ)    G) Gx) (uh (τ σ G)               Gx)]
+  [(uh ((ref τ)     (ref σ)     G) Gx) (uh (τ σ G)               Gx)]
+  [(uh (int         int         G) Gx) (uh G                     Gx)]
   
-  ;; (d) -- x occurs in τ case
-  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))]
+  ;; symbol clash
+  [(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
-  ;; (d) -- x does not occur in τ case
-  [(uh (x τ G) G_r boolean)
-   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
-   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  ;; occurs check
+  [(uh (x τ G) Gx) ⊥ (where #t (in-vars? x τ))]
   
-  ;; no rules applied; try next equation, if any.
-  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+  ;; variable elimination
+  [(uh (x τ G) Gx)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
 
 (define-metafunction stlc
   eliminate-G : x τ G -> G
@@ -255,14 +244,6 @@ It runs until there are no more changes. The (a), (b),
   [(in-vars-τ? x x) #t]
   [(in-vars-τ? x y) #f])
 
-(define-metafunction stlc
-  in-vars-G? : x G -> boolean
-  [(in-vars-G? x ·) #f]
-  [(in-vars-G? x (x τ G)) #t]
-  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
-                             (∨ (in-vars-τ? x τ)
-                                (in-vars-G? x G)))])
-
 (define-metafunction stlc
   apply-subst-τ : Gx τ -> τ
   [(apply-subst-τ · τ) τ]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt
index 03d4ebf1cc..9389f8bab5 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt
@@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
 
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
-  [(unify τ σ) (uh (τ σ ·) · #f)])
+  [(unify τ σ) (uh (τ σ ·) ·)])
 
 #|
 
-Algorithm copied from _An Efficient Unification Algorithm_ by 
-Alberto Martelli and Ugo Montanari (section 2).
-http://www.nsl.com/misc/papers/martelli-montanari.pdf
-
-This isn't the eponymous algorithm; it is an earlier one
-in the paper that's simpler.
+Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
+Unification Theory by Franz Baader and Wayne Synder
+http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
 
 The 'uh' function iterates over a set of equations applying the
-rules from the paper, moving them from the first argument to
-the second argument and tracking when something changes.
-It runs until there are no more changes. The (a), (b),
-(c), and (d) are the rule labels from the paper.
+rules from the paper, building up the result substitution in G_r.
 
 |#
 
 (define-metafunction stlc
-  uh : G G boolean -> Gx or ⊥
-
-  [(uh · G #t) (uh G · #f)]
-  [(uh · G #f) G]
+  uh : G Gx -> Gx or ⊥
   
-  ;; (a)
-  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  [(uh · Gx) Gx]
   
-  ;; (b)
-  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  ;; orient
+  [(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
   
-  ;; (c) -- term reduction
-  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
-  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  ;; trivial (other cases are covered by decomposition rule)
+  [(uh (x x G) Gx) (uh G Gx)]
   
-  ;; (c) -- failure
-  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  ;; decomposition
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
+  [(uh ((list τ)    (list σ)    G) Gx) (uh (τ σ G)               Gx)]
+  [(uh ((ref τ)     (ref σ)     G) Gx) (uh (τ σ G)               Gx)]
+  [(uh (int         int         G) Gx) (uh G                     Gx)]
   
-  ;; (d) -- x occurs in τ case
-  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  ;; symbol clash
+  [(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
-  ;; (d) -- x does not occur in τ case
-  [(uh (x τ G) G_r boolean)
-   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
-   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  ;; occurs check
+  [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
   
-  ;; no rules applied; try next equation, if any.
-  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+  ;; variable elimination
+  [(uh (x τ G) Gx)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
 
 (define-metafunction stlc
   eliminate-G : x τ G -> G
@@ -255,14 +244,6 @@ It runs until there are no more changes. The (a), (b),
   [(in-vars-τ? x x) #t]
   [(in-vars-τ? x y) #f])
 
-(define-metafunction stlc
-  in-vars-G? : x G -> boolean
-  [(in-vars-G? x ·) #f]
-  [(in-vars-G? x (x τ G)) #t]
-  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
-                             (∨ (in-vars-τ? x τ)
-                                (in-vars-G? x G)))])
-
 (define-metafunction stlc
   apply-subst-τ : Gx τ -> τ
   [(apply-subst-τ · τ) τ]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt
index 00af04e21a..07024185dd 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt
@@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
 
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
-  [(unify τ σ) (uh (τ σ ·) · #f)])
+  [(unify τ σ) (uh (τ σ ·) ·)])
 
 #|
 
-Algorithm copied from _An Efficient Unification Algorithm_ by 
-Alberto Martelli and Ugo Montanari (section 2).
-http://www.nsl.com/misc/papers/martelli-montanari.pdf
-
-This isn't the eponymous algorithm; it is an earlier one
-in the paper that's simpler.
+Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
+Unification Theory by Franz Baader and Wayne Synder
+http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
 
 The 'uh' function iterates over a set of equations applying the
-rules from the paper, moving them from the first argument to
-the second argument and tracking when something changes.
-It runs until there are no more changes. The (a), (b),
-(c), and (d) are the rule labels from the paper.
+rules from the paper, building up the result substitution in G_r.
 
 |#
 
 (define-metafunction stlc
-  uh : G G boolean -> Gx or ⊥
-
-  [(uh · G #t) (uh G · #f)]
-  [(uh · G #f) G]
+  uh : G Gx -> Gx or ⊥
   
-  ;; (a)
-  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  [(uh · Gx) Gx]
   
-  ;; (b)
-  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  ;; orient
+  [(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
   
-  ;; (c) -- term reduction
-  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
-  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  ;; trivial (other cases are covered by decomposition rule)
+  [(uh (x x G) Gx) (uh G Gx)]
   
-  ;; (c) -- failure
-  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  ;; decomposition
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
+  [(uh ((list τ)    (list σ)    G) Gx) (uh (τ σ G)               Gx)]
+  [(uh ((ref τ)     (ref σ)     G) Gx) (uh (τ σ G)               Gx)]
+  [(uh (int         int         G) Gx) (uh G                     Gx)]
   
-  ;; (d) -- x occurs in τ case
-  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  ;; symbol clash
+  [(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
-  ;; (d) -- x does not occur in τ case
-  [(uh (x τ G) G_r boolean)
-   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
-   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  ;; occurs check
+  [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
   
-  ;; no rules applied; try next equation, if any.
-  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+  ;; variable elimination
+  [(uh (x τ G) Gx)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
 
 (define-metafunction stlc
   eliminate-G : x τ G -> G
@@ -253,14 +242,6 @@ It runs until there are no more changes. The (a), (b),
   [(in-vars-τ? x x) #t]
   [(in-vars-τ? x y) #f])
 
-(define-metafunction stlc
-  in-vars-G? : x G -> boolean
-  [(in-vars-G? x ·) #f]
-  [(in-vars-G? x (x τ G)) #t]
-  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
-                             (∨ (in-vars-τ? x τ)
-                                (in-vars-G? x G)))])
-
 (define-metafunction stlc
   apply-subst-τ : Gx τ -> τ
   [(apply-subst-τ · τ) τ]
@@ -571,5 +552,5 @@ reachable from the given term.
                                (or (equal? red-t "error")
                                    (zero? n) (loop red-t (- n 1))))))))))))))
 
-(define small-counter-example (term ((λ x x) 1)))
+(define small-counter-example (term (λ x (x x))))
 (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt
index f954be062a..12fb6d34b1 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt
@@ -169,56 +169,45 @@ bring that type back, recurring on the continuation.
 
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
-  [(unify τ σ) (uh (τ σ ·) · #f)])
+  [(unify τ σ) (uh (τ σ ·) ·)])
 
 #|
 
-Algorithm copied from _An Efficient Unification Algorithm_ by 
-Alberto Martelli and Ugo Montanari (section 2).
-http://www.nsl.com/misc/papers/martelli-montanari.pdf
-
-This isn't the eponymous algorithm; it is an earlier one
-in the paper that's simpler.
+Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
+Unification Theory by Franz Baader and Wayne Synder
+http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
 
 The 'uh' function iterates over a set of equations applying the
-rules from the paper, moving them from the first argument to
-the second argument and tracking when something changes.
-It runs until there are no more changes. The (a), (b),
-(c), and (d) are the rule labels from the paper.
+rules from the paper, building up the result substitution in G_r.
 
 |#
 
 (define-metafunction stlc
-  uh : G G boolean -> Gx or ⊥
-
-  [(uh · G #t) (uh G · #f)]
-  [(uh · G #f) G]
+  uh : G Gx -> Gx or ⊥
   
-  ;; (a)
-  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  [(uh · Gx) Gx]
   
-  ;; (b)
-  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  ;; orient
+  [(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
   
-  ;; (c) -- term reduction
-  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
-  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  ;; trivial (other cases are covered by decomposition rule)
+  [(uh (x x G) Gx) (uh G Gx)]
   
-  ;; (c) -- failure
-  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  ;; decomposition
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
+  [(uh ((list τ)    (list σ)    G) Gx) (uh (τ σ G)               Gx)]
+  [(uh ((ref τ)     (ref σ)     G) Gx) (uh (τ σ G)               Gx)]
+  [(uh (int         int         G) Gx) (uh G                     Gx)]
   
-  ;; (d) -- x occurs in τ case
-  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  ;; symbol clash
+  [(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
-  ;; (d) -- x does not occur in τ case
-  [(uh (x τ G) G_r boolean)
-   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
-   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  ;; occurs check
+  [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
   
-  ;; no rules applied; try next equation, if any.
-  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+  ;; variable elimination
+  [(uh (x τ G) Gx)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
 
 (define-metafunction stlc
   eliminate-G : x τ G -> G
@@ -254,14 +243,6 @@ It runs until there are no more changes. The (a), (b),
   [(in-vars-τ? x x) #t]
   [(in-vars-τ? x y) #f])
 
-(define-metafunction stlc
-  in-vars-G? : x G -> boolean
-  [(in-vars-G? x ·) #f]
-  [(in-vars-G? x (x τ G)) #t]
-  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
-                             (∨ (in-vars-τ? x τ)
-                                (in-vars-G? x G)))])
-
 (define-metafunction stlc
   apply-subst-τ : Gx τ -> τ
   [(apply-subst-τ · τ) τ]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt
index 906e521b6a..ada35ec3dc 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt
@@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
 
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
-  [(unify τ σ) (uh (τ σ ·) · #f)])
+  [(unify τ σ) (uh (τ σ ·) ·)])
 
 #|
 
-Algorithm copied from _An Efficient Unification Algorithm_ by 
-Alberto Martelli and Ugo Montanari (section 2).
-http://www.nsl.com/misc/papers/martelli-montanari.pdf
-
-This isn't the eponymous algorithm; it is an earlier one
-in the paper that's simpler.
+Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
+Unification Theory by Franz Baader and Wayne Synder
+http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
 
 The 'uh' function iterates over a set of equations applying the
-rules from the paper, moving them from the first argument to
-the second argument and tracking when something changes.
-It runs until there are no more changes. The (a), (b),
-(c), and (d) are the rule labels from the paper.
+rules from the paper, building up the result substitution in G_r.
 
 |#
 
 (define-metafunction stlc
-  uh : G G boolean -> Gx or ⊥
-
-  [(uh · G #t) (uh G · #f)]
-  [(uh · G #f) G]
+  uh : G Gx -> Gx or ⊥
   
-  ;; (a)
-  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  [(uh · Gx) Gx]
   
-  ;; (b)
-  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  ;; orient
+  [(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
   
-  ;; (c) -- term reduction
-  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
-  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
-  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  ;; trivial (other cases are covered by decomposition rule)
+  [(uh (x x G) Gx) (uh G Gx)]
   
-  ;; (c) -- failure
-  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  ;; decomposition
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
+  [(uh ((list τ)    (list σ)    G) Gx) (uh (τ σ G)               Gx)]
+  [(uh ((ref τ)     (ref σ)     G) Gx) (uh (τ σ G)               Gx)]
+  [(uh (int         int         G) Gx) (uh G                     Gx)]
   
-  ;; (d) -- x occurs in τ case
-  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  ;; symbol clash
+  [(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
-  ;; (d) -- x does not occur in τ case
-  [(uh (x τ G) G_r boolean)
-   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
-   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  ;; occurs check
+  [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
   
-  ;; no rules applied; try next equation, if any.
-  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+  ;; variable elimination
+  [(uh (x τ G) Gx)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
 
 (define-metafunction stlc
   eliminate-G : x τ G -> G
@@ -253,14 +242,6 @@ It runs until there are no more changes. The (a), (b),
   [(in-vars-τ? x x) #t]
   [(in-vars-τ? x y) #f])
 
-(define-metafunction stlc
-  in-vars-G? : x G -> boolean
-  [(in-vars-G? x ·) #f]
-  [(in-vars-G? x (x τ G)) #t]
-  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
-                             (∨ (in-vars-τ? x τ)
-                                (in-vars-G? x G)))])
-
 (define-metafunction stlc
   apply-subst-τ : Gx τ -> τ
   [(apply-subst-τ · τ) τ]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt
index 30ed1ecbaa..edc863964b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt
@@ -97,7 +97,7 @@
 (test-equal (term (unify (list int) (list int)))
             (term ·))
 (test-equal (term (unify (int → x) (y → (list int))))
-            (term (y int (x (list int) ·))))
+            (term (x (list int) (y int ·))))
 (test-equal (term (unify (int → x) (x → (list int))))
             (term ⊥))
 (test-equal (term (unify (x   → (y          → x))
@@ -105,13 +105,13 @@
             (term ⊥))
 (test-equal (term (unify (x   → (y          → x))
                          (int → ((list int) → z))))
-            (term (x int (y (list int) (z int ·)))))
+            (term (z int (y (list int) (x int ·)))))
 (test-equal (term (unify (x   → (y          → z))
                          (int → ((list int) → x))))
-            (term (x int (y (list int) (z int ·)))))
+            (term (z int (y (list int) (x int ·)))))
 (test-equal (term (unify (x   → (y   → z))
                          (y   → (z   → int))))
-            (term (x int (y int (z int ·)))))
+            (term (z int (y int (x int ·)))))
 (test-equal (term (unify x (x → y)))
             (term ⊥))