No need for α-equivalent?; handled by Redex

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 t) ((reduce Δ t_0) (reduce Δ t_1)))
-   (where t_3 (reduce Δ t_1))
-   (side-condition (α-equivalent? t_2 t_3))
    ----------------- "≼-αβ"
    (convert Δ Γ t_0 t_1)]
 

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
+;; alpha-equivalent and subst tests
-;; ------------------------------------------------------------------------
+(check-equiv?
-(check-true
+ (term (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))
- (term
+ (term (Π (a : S) (Π (b : B) ((and S) B)))))
-  (α-equivalent?
-   (Π (a : S) (Π (b : B) ((and S) B)))
-   (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
 
 ;; Telescope tests
 ;; ------------------------------------------------------------------------