(define-type list (datatype (cons car::int cdr::list) nil)) (define x::list) (define y::list) (define y1::list) (define y2::list) (define y3::list) (define p::bool) (define q::bool) (assert (or p (= x (cons 10 y)))) (assert (= y y1)) (assert (= y1 y2)) (assert (= y2 y3)) (assert (or p (= y3 (cons 20 x)))) (assert (or p (not q))) (check)