ONCE_DEPTH_CONV : conv -> conv
# ONCE_DEPTH_CONV BETA_CONV `(\x. (\y. y + x) 1) 2`;; val it : thm = |- (\x. (\y. y + x) 1) 2 = (\y. y + 2) 1
# ONCE_DEPTH_CONV num_CONV `(\x. (\y. y + x) 1) 2`;; val it : thm = |- (\x. (\y. y + x) 1) 2 = (\x. (\y. y + x) (SUC 0)) (SUC 1)
CONV_TAC (ONCE_DEPTH_CONV BETA_CONV)
CONV_TAC (TOP_DEPTH_CONV BETA_CONV)