When applied to the goal (asl, w), the tactic Q.MATCH_RENAME_TAC q ls
parses the quotation q in the context of the goal, producing a term to use as
a pattern. The tactic then attempts a (first order) match of the pattern
against the term w.
For each variable v in the pattern, there will be an instantiation
term t, such that the substitution
produces w. The effect of the tactic is to then replace each t
with the corresponding v, yielding a new goal. Note that underscores
within a pattern, though strictly speaking variables, are not included
in this reverse instantiation.
pattern[v1 |-> t1, v2 |-> t2, ...]