Maps a theorem-tactic over the assumptions, applying first successful tactic.
FIRST_ASSUM ttac ([A1; ...; An], g)
has the effect of applying the first tactic which can be produced by
ttac from the ASSUMEd assumptions (A1 |- A1), ..., (An |- An) and which
succeeds when applied to the goal. Failures of ttac to produce a tactic are
Fails if ttac (Ai |- Ai) fails for every assumption Ai, or if the
assumption list is empty, or if all the tactics produced by ttac fail when
applied to the goal.