This is the analogue for definable functions of the function ``instantiate''.
The idea is to encode as sets the definable functions roughly as described in Chapter V of Kunen's *Set Theory*, except that you get to use any set as a starting point
(so instead of a countable number of functions you get a collection the same size as WF).

To understand ``elaborate'' you must think of a set as an encoding of a formula in a set theory with a very large term language
(every set in GS is a term).
The formula has free variables, and elaborate, given an assignment of values to free variables will give a truth value for
the encoded formula.

The first two clauses in the above definition concern atomic formulae (membership and equality), the terms of which are evaluated
using "instantiate".
The final clause addresses non-atomic formulae via a generalised scheffer stroke.