(define-type pos (subtype (v::int) (> v 0)))

(define x::pos)

(assert (= x 0))