MESON_TAC : thm list -> tactic
# g `(!x. x <= x) /\ (!x y z. x <= y /\ y <= z ==> x <= z) /\ (!x y. f(x) <= y <=> x <= g(y)) ==> (!x y. x <= y ==> f(x) <= f(y))`;;
# e(MESON_TAC[]);; 0..0..1..3..8..17..solved at 25 CPU time (user): 0. val it : goalstack = No subgoals
# g `!f:A->B s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)) <=> (?g. !x. x IN s ==> (g(f(x)) = x))`;;
# e(REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `?g:B->A. !y x. x IN s /\ y = f x ==> g y = x` THEN CONJ_TAC THENL [REWRITE_TAC[GSYM SKOLEM_THM]; AP_TERM_TAC THEN ABS_TAC]);; val it : goalstack = 2 subgoals (2 total) `(!y x. x IN s /\ y = f x ==> g y = x) <=> (!x. x IN s ==> g (f x) = x)` `(!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) <=> (!y. ?g. !x. x IN s /\ y = f x ==> g = x)`