HOL-ex.Function_Growth