(define-type R1 (record x::int y::int)) (define-type R2 (record idx::int flag::bool)) (define r1::R1) (define r2::R2) (assert (= (select r1 x) (select r2 idx))) (check)