Clarify when to unfold defined constants

SMT-LIB allows custom defined constants with define-fun. Currently it is unclear how the proofs for this have to look like.

If define-fun defines a function, it is also necessary to clarify how the β-reduction is done.

This is also relevant for the option that introduces skolems as defined constants. In general this is relevant if we want to allow certain SMT-LIB commands within proofs which extend the signature.