add qx_choose_then, qx_genl_tac, and qx_choosel_then to lcsymtacs

the latter two take a list of names to use for the quantified variables
at the top of the goal.
Add LAST_ASSUM and LAST_X_ASSUM tactics

like first_assum and first_x_assum, but work from the other end of the
assumption list