Böhm transformation
= Böhm transformation
{c}
A Böhm transformation is a finite composition of <capture-avoiding substitutions> and <lambda applications> to chosen auxiliary terms. It can extract a finite-address subtree of a <Böhm tree> as a substitution instance of the corresponding argument term.