[Enhancement request] useLemma with USubst or unification from Web UI

[rbohrer]

There are many cases where it would be helpful if we can apply a substitution when applying a lemma. By which I mean, if I have proved f()=f() for uninterpreted function symbol f(), it would be helpful if I can prove formulas of shape "Term = Term" by substituting "f() -> Term". Some of the main applications:

1. Sometimes we want to reuse the same lemma multiple times for different sub-programs, but each time it talks about different constants or variables (think component reuse in CoasterX)
2. Just like we use "abbrv" to simplify arithmetic proofs, you might want to prove a lemma using uninterpreted function symbols, then instantiate the symbols to some complicated terms, while still having a nice, fast proof.

In CoasterX, I did this sort of thing by manually writing Scala code that constructs a substitution and calls the low-level US rule. My question is: does the Web UI have any way to achieve the same results without custom Scala code? If not, would there be a reasonable way to add support? I imagine that unification in useLemma could be difficult (I remember that useLemma was already made more difficult because the lemma+substitution functionality is trickier on sequents than on formulas). As an alternative, I may be able to make it work if I could manually call the USubst tactics from the Web UI (or by typing them in the tactic window). But I wanted to ask before trying anything, because I assume the level of USubst support in the parsed language ranges somewhere between "not supported" to "not tested as thoroughly as other features".

Thanks!

Example attached. The first entry is a lemma. The second entry applies the lemma. The undesired behavior is that the second proof has an open goal because useLemma does not unify f() and g(). The specific formula is irrelevant - I just need something that had an easy proof, but wouldn't prove by "auto" when useLemma calls "auto".

UseLemmaQuestion.txt