Applies a list of tactics to the corresponding subgoals generated by a tactic.
DESCRIPTION
If T,T1,...,Tn are tactics, T THENL [T1,...,Tn] is a tactic which applies
T to a goal, and if it does not fail, applies the tactics T1,...,Tn to the
corresponding subgoals, unless T completely solves the goal.
FAILURE
The application of THENL to a tactic and tactic list never fails.
The resulting tactic fails if T fails when applied to the goal, or if
the goal list is not empty and its length is not the same as that of the
tactic list, or finally if Ti fails when applied to the i’th subgoal
generated by T.