`with .. unfold` wrongly binds at unit type

[mtzguido]

let my_pts_to (r : ref int) (x : int) : slprop = r |-> x

fn test (r : ref int)
  preserves my_pts_to r x
{
  with v. unfold my_pts_to r v;
  fold my_pts_to r v;
}

Fails highlighting the last use of v, saying:

- Could not instantiate implicits in term: my_pts_to r _
- Expected expression of type int got expression _ of type unit
- See also <input>:79.32-80.21

Doing this instead works fine:

fn test (r : ref int)
  preserves my_pts_to r x
{
  with v.
    assert my_pts_to r v;
  unfold my_pts_to r v;
  fold my_pts_to r v;
}