Function such_that 

pub fn such_that<T>(p: Mapping<T, bool>) -> T

Creates a logical value satisfying the property given by p.

This is also called the “epsilon operator”: its goal is not extract from ∃x. P(x) a x satisfying P.

(opaque)

requires

exists<x: T> p[x]

ensures

p[result]