THEN : TACTICALTHEN is a tactical.
(THEN tactic1 tactic2) will first apply tactic1; if it fails
then failure is returned, otherwise tactic2 is applied to each resulting
goal. If tactic2 fails on any of these goals, then failure is returned,
otherwise the new goals obtained from the calls to tactic2 are returned.
TPS documentation homepage