Prover failure when filling in squash arguments

[mtzguido]

This snippet:

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

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.