Function scope 

pub fn scope<'env, F, T>(f: F) -> T
where
    F: for<'scope> FnOnce(&mut Scope<'scope, 'env>) -> T,

Creusot wrapper around std::thread::scope.

requires

forall<s> inv(s) ==> f.precondition((s,))

ensures

exists<s> inv(s) && f.postcondition_once((s,),result)