MATCH_ASMSUB_RENAME_TAC : term quotation -> string list -> tactic
In either case, the match will return an instantiation mapping the fresh free variables of pat to terms occurring in the goal. This instantiation drops its bindings for variables whose names begin with an underscore, is next reversed, and is finally applied to the goal. This will both cause free variables in the goal to be renamed, and for larger terms to be replaced by variables (similar to what happens with the use of SPEC_TAC).
> Q.MATCH_ASMSUB_RENAME_TAC `x < n` ([``P(y < m):bool``, ``Q(x < z) : bool``], ``x + z < 10``); val it = ([([``P (y < m)``, ``Q (x < n)``], ``x + n < 10``)], fn): goal list * validation