SYM_CONV : term -> thm
|- t1 = t2 <=> t2 = t1
# SYM_CONV `2 = x`;; val it : thm = |- 2 = x <=> x = 2