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