Have iApply introduce equalities for subterms that cannot be unified directly
The initial motivation is to be able to go from a proof-mode goal of the form:
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
to
--------------------------------------∗
⌜x4 = z⌝
without relying explicitly on the names x4
and z
.
I'm not sure what would be the most general form of such a tactic, or what its user interface would be, though. I think it would be nice to have it as an instance of iApply
, if that's possible. (having it in iFrame
as well is perhaps possible but risky, for instance in the case of mapsto it should at least be restricted to mapsto with the same syntactic location...).