mathlib
6d98ae04 - Added proof that taking a step increases a stack size by at most the function length
