PART_MATCH_A : (term -> term) -> thm -> term -> thm
STRUCTURE
SYNOPSIS
Instantiates a theorem by matching part of its conclusion to a term.
DESCRIPTION
PART_MATCH_A behaves as PART_MATCH except that it permits instantiating variables which appear in the assumptions of the given theorem.
SEEALSO
HOL  Kananaskis-14