Function forall 

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

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

Example:

The Rust expression forall(|x: T| phi(x)) corresponds to ∀ (x: T), phi(x).