function (result) requires (and (skiplist? sls) ((skiplist-item? sls) item)) ensures (boolean? result)