Pulse cannot infer permission on record field when permission involves existential quantification about steel HOT 2 CLOSED

let rec_perm_existential (r:my_rec) : vprop 
  = exists* s. A.pts_to r.a s

```pulse
fn rewrite_existential (a: A.array U8.t)
  requires exists* s. A.pts_to a s
  returns r:my_rec
  ensures rec_perm_existential r
{
  let r = mk_rec a;
  with s. rewrite (A.pts_to a s)
               as (A.pts_to r.a s);
  rewrite (exists* s. A.pts_to r.a s)
       as (rec_perm_existential r);
  r
}