(define-type PC (scalar pc1 pc2 pc3))
(define x::(subtype (y::PC) (or (= y pc1) (= y pc2))))
;; (define x::PC)

(assert (/= x pc1))
(assert (/= x pc2))
(check)