(define f::(-> int int))
(define a::int)
(assert (forall (x::int) (>= (f x) 0)))
(assert (= (f a) a))
(check)