NUM_EQ_CONV : conv
|- (n = m) <=> T or |- (n = m) <=> F
# NUM_EQ_CONV `1 = 2`;; val it : thm = |- 1 = 2 <=> F # NUM_EQ_CONV `12 = 12`;; val it : thm = |- 12 = 12 <=> T