Rollup merge of #124540 - compiler-errors:nested-goals, r=lcnr

Give proof tree visitors the ability to instantiate nested goals directly

Useful when we want to look at the nested goals but not necessarily visit them (e.g. in select).

r? lcnr

Author: matthiaskrgr