(define-type S (scalar s1 s2 s3)) (define-type T int) (define f1::(-> S T)) (define f2::(-> S T)) (assert (= (f1 s1) (f2 s1))) (assert (= (f1 s2) (f2 s2))) (assert (/= f1 f2)) (check)