Badge-userfn
Undefined function used by badge on non-primitives
When badge is given a non-primitive function symbol fn
it calls this function to determine the badge of fn. 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, badge-userfn has an attachment that makes it behave
as though all warrants are assumed. See badge for details.
