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)