(define-type tree (datatype (mk-node val::int left::tree right::tree) leaf)) (define x1::tree) (define x2::tree) (define x3::tree) (define x4::tree) (assert (= x1 (mk-node 10 x2 x3))) (assert (= x4 (mk-node 20 leaf x1))) (assert (= x2 x4))