Tactical.goal

An application of goal_assum ttac to the goal (A,w0) can be seen as a tactic that first transforms the goal into (w1::A,F) (as if starting a proof by contradiction, normalising ¬w0 into an equivalent w1); pops the new assumption w1 and applies the theorem-tactic ttac to this theorem (w1 ⊢ w1); and when this completes, renormalises the conclusion of the goal if it has turned into something of the form w2 ⇒ F.

The first normalisation phase will turn something of the form ¬p into p⇒F, and will also flip outermost existential quantifiers into universals. Thus, if the w0 term was ∃x. P x ∧ Q (f x), the w1 term will be ∀x. P x ∧ Q (f x) ⇒ F. The second normalisation phase will undo this, so that if the effect of ttac is equivalent to a call of MP_TAC th' with th' a universally quantified implication into falsity, then the goal will again become an existentially quantified conjunction.