(define-type R (record x::bool y::bool)) (define t1::R) (define t2::R) (define t3::R) (define t4::R) (define t5::R) (assert (/= t1 t2)) (assert (/= t1 t3)) (assert (/= t1 t4)) (assert (/= t1 t5)) (assert (/= t2 t3)) (assert (/= t2 t4)) (assert (/= t2 t5)) (assert (/= t3 t4)) (assert (/= t3 t5)) (assert (/= t4 t5)) (check)