LAST_X_ASSUMTactical.LAST_X_ASSUM : thm_tactic -> tacticMaps a theorem-tactic over the assumptions, in reverse order, applying first successful tactic and removing the assumption that gave rise to the successful tactic.
LAST_X_ASSUM behaves like FIRST_X_ASSUM,
except that it goes through the list of assumptions in reverse order