Apply$-userfn
Undefined function used by apply$ on non-primitives
When apply$ is given a non-primitive function symbol it calls
this function to determine the results of applying that symbol to the given
arguments. But this function is undefined. In the proof theory, its value
on a given function symbol fn is specified, if at all, by the warrant for fn which must be available as a hypothesis in the formula
being proved. In the evaluation theory, apply$-userfn has an
attachment that makes it behave as though all warrants are assumed. See
apply$ for details.
