Join the two mechanisms that do "Unification with abstraction" around in substitution trees

[quickbeam123]

From Ahmed:

"The VSpecialVar mechanism is not to do with applicative terms, but linked to a unification with abstraction type of thing that we use in higher-order mode. I have long thought that we should combine it with unification with abstraction instead of having two mechanisms.

I can illustrate it with an example. Imagine that we have terms p(8) and ~p(2y). Instead of inserting these terms into the indices, we would insert terms p(#1) and ~p(#2) into the indices where #1 and #2 are the so-called VSpecialVars. They need to be disjoint from both normal vars and special variables. Outside the indices, we maintain a mapping from very special vars to the terms they represent (I can't recall what we do about alpha-equivalence).

When attempting to unify the terms, we succeed and produce the constraint #1 != #2. Dereferencing the very special variable then gives us the actual constraint 8 != 2y."

"As noted above, we should really merge the two unification with abstraction mechanism currently functional in Vampire. From before, I recall thinking that the mechanism I outline above is cleaner than the other mechanism, but if this is mistaken we can go with the other mechanism."

[MichaelRawson]

I don't think we have "very special" variables any more - should this be closed?