Got the right function computing length for the iterated bound substitution and started with program extraction
This reverts commit 20758037.