MONO_TAC : tactic
# g `(!x. P x ==> Q x) ==> (?y. P y /\ ~Q y) ==> (?y. Q y /\ ~P y)`;; ...
# e STRIP_TAC;; val it : goalstack = 1 subgoal (1 total) 0 [`!x. P x ==> Q x`] `(?y. P y /\ ~Q y) ==> (?y. Q y /\ ~P y)`
# e MONO_TAC;; val it : goalstack = No subgoals