SUBS_CONV : thm list -> term -> thm
# SUBS_CONV[ARITH_RULE `x + 0 = x`] `(x + 0) + (y + 0) + (x + 0) + (0 + 0)`;; val it : thm = |- (x + 0) + (y + 0) + (x + 0) + 0 + 0 = x + (y + 0) + x + 0 + 0
# REWRITE_CONV[ARITH_RULE `x + 0 = x`] `(x + 0) + (y + 0) + (x + 0) + (0 + 0)`;; val it : thm = |- (x + 0) + (y + 0) + (x + 0) + 0 + 0 = x + y + x