Apply a theorem tactic to named assumption, removing the assumption.
DESCRIPTION
The tactic REMOVE_THEN "name" ttac applies the theorem-tactic ttac to the
assumption labelled name (or the first in the list if there is more than
one), removing the assumption from the goal.
FAILURE CONDITIONS
Fails if there is no assumption of that name or if the theorem-tactic fails
when applied to it.
EXAMPLE
See LABEL_TAC for a relevant example.
USES
Using an assumption identified by name that will not be needed again in the
proof.