Pulse existential inference fails when struct field appears in separation logic predicate

[gebner]

Pulse's existential witness inference fails when an ensures clause has the pattern:

 exists* (v0: my_struct). pts_to s v0 ** pts_to v0.b ...

After a field write, Pulse tries to prove Mkmy_struct v0.b x == v0 instead of instantiating the existential with the new struct value {b = v0.b; c = x}.

Minimal reproducer (self-contained, only depends on Pulse.Lib.Reference):

 module Issue113
 open Pulse
 open Pulse.Lib.Reference
 #lang-pulse
 
 noeq type my_struct = { b: ref int; c: int; }
 
 assume val struct_unfolded ([@@@Pulse.Lib.Core.mkey] x: ref my_struct) (p: perm) : slprop
 assume val struct_b_field (x: ref my_struct) : GTot (ref (ref int))
 assume val struct_c_field (x: ref my_struct) : GTot (ref int)
 
 [@@Pulse.Lib.Core.pulse_intro]
 assume val struct_unfold (x: ref my_struct) (#p: perm) (vx: my_struct) :
   stt_ghost unit emp_inames
     (pts_to x #p vx)
     (fun _ ->
       struct_unfolded x p **
       pts_to (struct_b_field x) #p vx.b **
       pts_to (struct_c_field x) #p vx.c)
 
 [@@Pulse.Lib.Core.pulse_intro]
 assume val struct_fold (x: ref my_struct) (#p: perm) (v_b: ref int) (v_c: int) :
   stt_ghost unit emp_inames
     (struct_unfolded x p **
      pts_to (struct_b_field x) #p v_b **
      pts_to (struct_c_field x) #p v_c)
     (fun _ -> pts_to x #p { b = v_b; c = v_c })
 
 [@@Pulse.Lib.Core.pulse_impure_spec_no_proof_required]
 assume val get_c (x: ref my_struct) (#p: perm) :
   stt_atomic (ref int)
     #PulseCore.Observability.Neutral
     emp_inames
     (struct_unfolded x p)
     (fun r -> struct_unfolded x p ** Pulse.Lib.Core.rewrites_to r (struct_c_field x))
 
 // FAILS with: pts_to s (Mkmy_struct v0.b x) == pts_to s v0
 fn write_c (s: ref my_struct) (x: int)
   requires exists* (v0: my_struct). pts_to s v0 ** pts_to v0.b v0.c
   ensures  exists* (v0: my_struct). pts_to s v0 ** pts_to v0.b v0.c
 {
   (get_c s) := x;
 }

Tested with F* nightly-2026-05-27. Discovered via FStarLang/pal#113.