Interpret `**` on both sides of `@==>` to allow inferring implicit arguments to stick lemmas about steel HOT 1 OPEN

I have a fix to at least the main symptom reported in this issue. However, keep in mind that the Pulse unifier is, by design, very simple, e.g., it does not backtrack.

So, see 80a3d28 for a test case which shows what you can expect to work and not.

That said, there is one aspect of it that I had been trying to get to work, which I think ought to work eventually, but is hard to do in the current way the prover is structured. Consider this example:

ghost
fn test_elim_3 (p q r:vprop)
requires ((p ** q) @==> r) ** p ** q
ensures r
{
    elim _ _;
}

Say the invocation of elim is really elim ?1 ?2, to give names to those uvars.
The prover is called with the following goals : ?1 @==> ?2 and ?1.
The unifier correctly solves the first goal, setting ?1 := p ** q and ?2 := r.
Now it recurses trying to check that the second goal ?1 := p ** q is properly solved.
But this goal is not an atomic vprop and the matcher is currently designed to solve things one atomic vprop at a time, trying to match it against atomic vprops from the context. So, this fails.
@aseemr : would be nice to talk through this; seems to require some non-trivial restructuring of the matcher and its invariants ... but perhaps you know of an easier way.

from steel.