Names for variables introduced by STApp

[mtzguido]

A follow up to #88, also give a clearer name to the implicits introduced by the Pulse checker on applications, i.e. those at the tail of a function call. This does not do anything for implicits "inside" an application, since those are instantiated by F*. Perhaps this PR is better not merged until we fix those too, so we do not create confusion?
 
File:

module X

open Pulse.Lib.Pervasives

assume val f : int -> vprop

```pulse
fn foo () (#x:int)
  requires f x
  ensures  emp
{
  admit()
}
```

```pulse
fn test (x:int)
  requires emp
  ensures  emp
{
  foo ()
}
```

Before:

* Error <unknown> at X.fst(21,2-21,8):
  - Cannot prove:
      X.f _
  - In the context:
      emp

After:

* Error <unknown> at X.fst(21,2-21,8):
  - Cannot prove:
      X.f ?x
  - In the context:
      emp