clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;