admit seems to affect code before it

[mtzguido]

This snippet works, even if it seems to be introducing an exists* (x:unit). Pure False.

```pulse
fn
test_intro (_:unit)
  requires emp
  ensures emp
{
  intro_exists (fun () -> pure False) ();
  admit()
}
```

Removing the admit makes it fail as it should.

```pulse
fn
test_intro (_:unit)
  requires emp
  ensures emp
{
  intro_exists (fun () -> pure False) ()
}
```

Puzzlingly, if I try to print the state before the admit, it seems as if intro_exists was not applied since it is bound at type stt_ghost.

```pulse
fn
test_intro (_:unit)
  requires emp
  ensures emp
{
  intro_exists (fun () -> pure False) ();
  show_proof_state;
  admit()
}
```

  - Tactic logged issue:
  - Current context:
      emp ** 
      emp
  - In typing environment:
      [_#2 : stt_ghost unit emp_inames (pure l_False) (fun _ -> exists* (_: unit). pure l_False),
      uu___85#1 : unit]

[nikswamy]

I think the problem is because the type of intro_exists is not interpreted properly in Pulse, since it uses a kind of points-free style of specification, which Pulse doesn't expect.