Unfold cannot unfold local slprop definitions

[gebner]

module LocalUnfold
#lang-pulse
open Pulse

fn foo (x: ref nat) (vx0: erased nat)
  requires pts_to x vx0
  ensures exists* (vx: nat). pts_to x vx
{
  let my_inv = (fun (k: nat) -> pts_to x k);
  fold my_inv vx0; // Cannot unfold my_inv vx0, the head is not an fvar
  unfold my_inv;
}

[gebner]

I found a workaround:

fn bar (x: ref nat) (vx0: erased nat)
  requires pts_to x vx0
  ensures exists* (vx: nat). pts_to x vx
{
  with my_inv. assert pure (my_inv == fun k -> pts_to x k);
  assert my_inv vx0;
}