(define x::int) (define y::int) (define z::int) (define f::(-> int int)) (assert (/= (f (+ x 2)) (f (- y 1)))) (assert (= x (- y 4))) (check)