Function exists

pub fn exists<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop

The existential quantifier. This should be used only for Hax code: in Rust, this is always true.

Example:

The Rust expression exists(|x: T| phi(x)) corresponds to ∃ (x: T), phi(x).