= Böhm-out lemma
{c}
For a finite path in a <Böhm tree>, choose $q$ at least the head arity at every preceding node. Replace relevant variables by $U_q=\lambda z_1\cdots z_q w.wz_1\cdots z_q$. After exposing each node, supply its initial bound variables with $U_q$, pad its $m$ arguments to $q$, and apply the projection $\lambda z_1\cdots z_q.z_i$ selecting the next child. Each step returns that child with accumulated substitutions, so iteration reaches a substitution instance of the chosen subtree. Tupling preserves all children until selection, even when the same variable occurs at several nodes.
Back to article page
