(define-type u)
(define f1::(-> u bool))
(define f2::(-> u u bool))
(define x1::u)
(define x2::u)
(define x3::u)
(define x4::u)
(define x5::u)
(define x6::u)
(define p0::bool)
(define p1::bool)
(define p2::bool)
(define foo::(-> bool u))

(assert (/= (foo p0) (foo p1)))
(assert (/= (foo p0) (foo p2)))
(assert (/= (foo p1) (foo p2)))
(check)