SELECT_CONV : term -> thm
# SELECT_CONV `(@n. n < m) < m`;; val it : thm = |- (@n. n < m) < m <=> (?n. n < m)
# g `!m. 0 < m ==> (@n. n < m) < SUC m`;;
# e(REPEAT STRIP_TAC THEN MATCH_MP_TAC(ARITH_RULE `!m n. m < n ==> m < SUC n`));; val it : goalstack = 1 subgoal (1 total) 0 [`0 < m`] `(@n. n < m) < m`
# e(CONV_TAC SELECT_CONV);; val it : goalstack = 1 subgoal (1 total) 0 [`0 < m`] `?n. n < m`