Solution (source code)

= Solution

A <nice forcing name> for a <subset> of a ground-model set $a$, often an <ordinal>, has the form
$$
\boxed{\sigma=\{(\check x,q):x\in a,\ q\in A_x\},}
$$
where each $A_x$ is an antichain in $\mathbb Q$ and the entire construction belongs to $M$. Its value consists of the $x$ for which $H$ meets $A_x$. The antichains need not be maximal. Under the countable chain condition they are countable in $M$, which makes <nice forcing names> useful for counting possible <subsets> in extensions.