Functions that are defined as @extern can use non-purescala features
within their body. Leon will reason about them according to their
specification (the unknown body becomes a hole and then a choose).