BINDER_CONV : conv -> term -> thm
# BINDER_CONV SYM_CONV `@n. n = m + 1`;; val it : thm = |- (@n. n = m + 1) = (@n. m + 1 = n) # BINDER_CONV (REWR_CONV SWAP_FORALL_THM) `!x y z. x + y + z = y + x + z`;; val it : thm = |- (!x y z. x + y + z = y + x + z) <=> (!x z y. x + y + z = y + x + z)