(declare-datatypes (T!0) ((List!6 (Nil!3) (Cons!3 (h!48 T!0) (t!55 (List!6 T!0))))))

(declare-const domain!0 (List!6 Int))

(define-fun-rec (par (T!90) (content!0 ((thiss!113 (List!6 T!90))) (Set T!90) (ite (is-Nil!3 thiss!113) (as emptyset T!90) (union (insert (as emptyset T!90) (h!48 thiss!113)) (content!0 (t!55 thiss!113)))))))

(define-fun-rec (par (T!47) (contains!0 ((thiss!33 (List!6 T!47)) (v!0 T!47)) Bool (let ((x$2!2 (ite (is-Cons!3 thiss!33) (or (= (h!48 thiss!33) v!0) (contains!0 (t!55 thiss!33) v!0)) false))) (assume (= x$2!2 (member v!0 (content!0 thiss!33))) x$2!2)))))

(declare-const k!0 Int)

(assert (not (=> (and (is-Cons!3 domain!0) (contains!0 domain!0 k!0) (=> (contains!0 (t!55 domain!0) k!0) false)) false)))

(check-sat)

; check-assumptions required here, but not part of tip standard