PART_MATCH_ADrule.PART_MATCH_A : (term -> term) -> thm -> term -> thmInstantiates a theorem by matching part of its conclusion to a term.
PART_MATCH_A behaves as PART_MATCH except
that it permits instantiating variables which appear in the assumptions
of the given theorem.