DEPTH_CONV : conv -> conv
# DEPTH_CONV BETA_CONV `(\x. (\y. y + x) 1) 2`;; val it : thm = |- (\x. (\y. y + x) 1) 2 = 1 + 2
# DEPTH_CONV BETA_CONV `(\f x. (f x) + 1) (\y.y) 2`;; val it : thm = |- (\f x. f x + 1) (\y. y) 2 = (\y. y) 2 + 1
# DEPTH_CONV BETA_CONV `(\f x. (f x)) (\y.y) 2`;; val it : thm = |- (\f x. f x) (\y. y) 2 = 2
# DEPTH_CONV NUM_ADD_CONV `(1 + 2) + (3 + 4 + 5)`;; val it : thm = |- (1 + 2) + 3 + 4 + 5 = 15