#lang racket
(require redex)

(define-language vars
  (x variable-not-otherwise-mentioned))

(define-judgment-form vars
  #:mode(equal I O)
  #:contract(equal x x)
  [(equal x x)])

(define-metafunction vars
  different : any any -> any
  [(different x x) #f]
  [(different x_0 x_1) #t])

(define-judgment-form vars
  #:mode(excludes I I)
  #:contract(excludes x (x ...))
  [(excludes x ())]
  [(excludes x_0 (x_2 ...))
   (side-condition (not (judgment-holds (equal (term x_0) (term x_1)))))
   ;(where #f (judgment-holds (equal x_0 x_1)))
   ---
   (excludes x_0 (x_1 x_2 ...))]
  )


(judgment-holds (excludes t ()))
(judgment-holds (excludes t (t)))
(judgment-holds (excludes t (x)))