Avigail provided a draft proposal (see First Draft, below). Klaus suggested (here) that we shouldn't clutter the language with additional built-in functions, but rather should use free variables.
In the Dec 21st meeting, we agreed to adopt the new built-in functions. Erich suggested that the proposed built-in functions for non-determinism seem to be related to forall declarations, and that we should align the syntax and semantics of the two areas to the extent possible.