Function spawn 

pub fn spawn<F, T>(f: F) -> JoinHandle<T>
where
    F: FnOnce(Ghost<Tokens<'_>>) -> T + Send + 'static,
    T: Send + 'static,

Creusot wrapper around std::thread::spawn.

The only difference is that the closure gives access to a fresh token object