LAST_X_ASSUM : thm_tactic -> tactic
STRUCTURE
SYNOPSIS
Maps a theorem-tactic over the assumptions, in reverse order, applying first successful tactic and removing the assumption that gave rise to the successful tactic.
DESCRIPTION
LAST_X_ASSUM behaves like FIRST_X_ASSUM, except that it goes through the list of assumptions in reverse order
SEEALSO
HOL  Kananaskis-13