UNIFY_ACCEPT_TAC : term list -> thm -> 'a * term -> ('b list * instantiation) * 'c list * (instantiation -> 'd list -> thm)
# g `(?x:num. p(x) /\ q(x) /\ r(x)) ==> ?y. p(y) /\ (q(y) <=> r(y))`;;
# e STRIP_TAC;; val it : goalstack = 1 subgoal (1 total) 0 [`p x`] 1 [`q x`] 2 [`r x`] `?y. p y /\ (q y <=> r y)`
# e (X_META_EXISTS_TAC `n:num` THEN CONJ_TAC);; val it : goalstack = 2 subgoals (2 total) 0 [`p x`] 1 [`q x`] 2 [`r x`] `q n <=> r n` 0 [`p x`] 1 [`q x`] 2 [`r x`] `p n`
# e(FIRST_X_ASSUM(UNIFY_ACCEPT_TAC [`n:num`]));; val it : goalstack = 1 subgoal (1 total) 0 [`p x`] 1 [`q x`] 2 [`r x`] `q x <=> r x`
# e(ASM_REWRITE_TAC[]);; val it : goalstack = No subgoals