MESON : thm list -> term -> thm
# MESON[] `!P. P F /\ P T ==> !x. P x`;; ... val it : thm = |- !P. P F /\ P T ==> (!x. P x)
# MESON[REAL_NEG_NEG] `(!x. P(--x)) ==> !x:real. P x`;; ... val it : thm = |- (!x. P (--x)) ==> (!x. P x)
# MESON[] `(!x. P(--x)) ==> !x:real. P x`;; ... Exception: Failure "solve_goal: Too deep".