'could not prove uvar' when there is existential in post

[mtzguido]

This fails

module Bug163

open Pulse.Lib.Pervasives

```pulse
fn test (z:int)
  requires emp
  returns _:unit
  ensures (exists* (x:int). emp)
{
  ();
}

with:

proof-state: State dump @ depth 8 (at the time of failure):
Location: Pulse.Typing.Env.fst(405,2-405,31)
* Error 228 at ../../examples/pulse/bug-reports/Bug163.fst(5,8-5,8):
  - Tactic failed
  - "Pulse checker failed"
  - See also Pulse.Typing.Env.fst(405,2-405,31)

* Error <unknown> at ../../examples/pulse/bug-reports/Bug163.fst(11,2-11,4):
  - Tactic logged issue:
  - resulted substitution after intro exists protocol is not well-typed: prover could not prove uvar _#2

even if the body is admit(); or if we try to manually introduce the exists.

[mtzguido]

Pulse is no longer here.