ITAUT_TAC : tactic
# g `!p q. (p ==> q) <=> (~q ==> ~p)`;;
# e(REPEAT GEN_TAC THEN EQ_TAC);; val it : goalstack = 2 subgoals (2 total) `(~q ==> ~p) ==> p ==> q` `(p ==> q) ==> ~q ==> ~p`
# e ITAUT_TAC;; ... val it : goalstack = 1 subgoal (1 total) `(~q ==> ~p) ==> p ==> q`
# e(MESON_TAC[]);; val it : goalstack = No subgoals