Sub-term to free variable lifting tactic

[Xaphiosis]

When we try to make a rule to match a complex goal, we often want something like epptr in the rule, but we have PTR(endpoint_C) (capEPPtr (projr luRet))) or whatever. It would be really cool to have a tactic that can create a new free var somehow, and then replace every instance of a term in the goal with that var.

@lsf37 commented:

It would be useful to have, and something like it must be possible, because Norbert's vcg does this -- it replaces x_' s with a green x in goals. So something somewhere must be doing that substitution. Probably a bit of a rabbit hole, but might be worth making an issue for.