Prover failure when filling in squash arguments

[mtzguido]

This snippet:

```pulse
ghost
fn f (p:prop)
     (#_ : squash p)
  requires emp
  ensures emp
{
  ();
}
```

```pulse
ghost
fn g (p:prop)
  requires pure p
  ensures emp
{
  f p
}
```

Gives an error in the call to f:

- Prover error: ill-typed substitutions (prover could not prove uvar _#3)
- pst.pg = [_#2 : squash p, p#1 : prop]
- pst.uvs = [?uu___24309#3 : squash p]
- pst.ss = []
- pst.remaining_ctxt = []
- pst.unsolved = []

But changing that line to:

  f p #()

works perfectly fine.