If U is a universe name different from Reserve, v is a variable and
is a rule then the following expression is a rule with main
existential variable v that ranges over U and body
:
choose v in U
endchoose
This is the basic version of the choice constructor; a stronger version is defined in 4.2.2. Perspicuity is defined as 3.2.