(define t::(record x::int y::(subtype (y::int) (> y x)))) (assert (= (select t x) 0)) (check)