diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt
index e5967d7..389726e 100644
--- a/cur-lib/cur/curnel/redex-core.rkt
+++ b/cur-lib/cur/curnel/redex-core.rkt
@@ -61,11 +61,6 @@
    ----------------
    (unv-pred (Unv i_1) (Unv i_2) (Unv i_3))])
 
-(define-metafunction ttL
-  α-equivalent?  : t t -> #t or #f
-  [(α-equivalent? t_0 t_1)
-   ,(alpha-equivalent? ttL (term t_0) (term t_1))])
-
 ;; Replace x by t_1 in t_0
 (define-metafunction ttL
   subst : t x t -> t
@@ -362,9 +357,7 @@
    ----------------- "≼-Unv"
    (convert Δ Γ (Unv i_0) (Unv i_1))]
 
-  [(where t_2 (reduce Δ t_0))
-   (where t_3 (reduce Δ t_1))
-   (side-condition (α-equivalent? t_2 t_3))
+  [(where (t t) ((reduce Δ t_0) (reduce Δ t_1)))
    ----------------- "≼-αβ"
    (convert Δ Γ t_0 t_1)]
 
diff --git a/cur-test/cur/tests/redex-core.rkt b/cur-test/cur/tests/redex-core.rkt
index 6b6a291..cb53f66 100644
--- a/cur-test/cur/tests/redex-core.rkt
+++ b/cur-test/cur/tests/redex-core.rkt
@@ -16,7 +16,7 @@
 (define-syntax-rule (check-not-equiv? e1 e2)
   (check (compose not (default-equiv)) e1 e2))
 
-(default-equiv (lambda (x y) (term (α-equivalent? ,x ,y))))
+(default-equiv (curry alpha-equivalent? ttL))
 
 ;; Syntax tests
 ;; ------------------------------------------------------------------------
@@ -73,13 +73,10 @@
 (check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
 
 
-;; α-equiv and subst tests
-;; ------------------------------------------------------------------------
-(check-true
- (term
-  (α-equivalent?
-   (Π (a : S) (Π (b : B) ((and S) B)))
-   (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
+;; alpha-equivalent and subst tests
+(check-equiv?
+ (term (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))
+ (term (Π (a : S) (Π (b : B) ((and S) B)))))
 
 ;; Telescope tests
 ;; ------------------------------------------------------------------------