FIRST_PROVE
Tactical.FIRST_PROVE : (tactic list -> tactic)
Applies the first tactic in a tactic list which completely proves the goal.
When applied to a list of tactics [T1;...;Tn], and a goal g, the
tactical FIRST_PROVE tries applying the tactics to the goal until one
proves the goal. If the first tactic which proves the goal is Tm, then
the effect is the same as just Tm. Thus FIRST_PROVE effectively
behaves as follows:
FIRST_PROVE [T1;...;Tn] = (T1 THEN NO_TAC) ORELSE ... ORELSE (Tn THEN NO_TAC)
Failure
The application of FIRST_PROVE to a tactic list never fails. The
resulting tactic fails iff none of the supplied tactics completely
proves the goal by itself, or if the tactic list is empty.