THEN** : TACTICALTHEN** is a tactical.
(THEN** tactic1 tactic2) will first apply tactic1 to the current
goal. If it does not fail, tactic2 will be applied to the goals which are
produced by tactic1, and success will be returned along with any new goals
produced. If tactic1 fails, failure will be returned. Differs from THEN
and THEN* in that the current goal will never be copied.
TPS documentation homepage