(define t::(tuple x::int (subtype (y::int) (> y x))))
(define x::int)
(assert (= (select t 1) x))
(check)