Given a theorem-tactic ttac and a goal (A,t), PSTRIP_GOAL_THEN removes one
outermost occurrence of one of the connectives !, ==>, ~ or /\ from the
conclusion of the goal t. If t is a universally quantified term, then
STRIP_GOAL_THEN strips off the quantifier. Note that PSTRIP_GOAL_THEN
will strip off paired universal quantifications.
where p' is a primed variant that contains no variables that
appear free in the assumptions A. If t is a conjunction,
then PSTRIP_GOAL_THEN simply splits
the conjunction into two subgoals:
A ?- !p. u
============== PSTRIP_GOAL_THEN ttac
A ?- u[p'/p]
If t is an implication "u ==> v" and if:
A ?- v /\ w
================= PSTRIP_GOAL_THEN ttac
A ?- v A ?- w
A ?- v
=============== ttac (u |- u)
A' ?- v'
Finally, a negation ~t is treated as the implication t ==> F.
A ?- u ==> v
==================== PSTRIP_GOAL_THEN ttac
A' ?- v'