HINT_EXISTS_TAC : tactic
# g `!P Q R S. P 1 /\ Q 2 /\ R 3 ==> ?x y. P x /\ R y /\ S x y`;; val it : goalstack = 1 subgoal (1 total) `!P Q R S. P 1 /\ Q 2 /\ R 3 ==> (?x y. P x /\ R y /\ S x y)` # e HINT_EXISTS_TAC;; val it : goalstack = 1 subgoal (1 total) `!P Q R S. P 1 /\ Q 2 /\ R 3 ==> S 1 3`