LAST_ASSUM
Tactical.LAST_ASSUM : (thm_tactic -> tactic)
Maps a theorem-tactic over the assumptions, in reverse order, applying first successful tactic.
LAST_ASSUM behaves like FIRST_ASSUM, except that it goes through the
list of assumptions in reverse order