Spec quantifiers (forall, exists)

Quantifiers are explained in the Quantifiers part of the tutorial. Specifically, forall is explained in forall and triggers and exists is explained in exists and choose.