Assuming $\mathrm{PFA}$, we shall use internally club $\omega _1$ -guessing models as side conditions to show that for every tree T of height $\omega _2$ without cofinal branches, there is a proper and $\aleph _2$ -preserving forcing notion with finite conditions which specialises T. Moreover, the forcing has the $\omega _1$ -approximation property.

Starting with two supercompact cardinals we produce a generic extension of the universe in which a principle that we call GM+ holds. This principle implies ISP and ISP, and hence th...