pure in assert_ does not work (Pulse)

[tdardinier]

Pulse treats pure (...) in asserts in an opaque way. As an example, Pulse is not able to verify a statement like assert_ (pure (5 = 5));. It fails with the following error message:

(Error) Failed to prove the following goals:
... Steel.ST.Util.pure (Prims.op_Equality 5 5)
The remaining conjuncts in the separation logic context available for use are:...

This behavior also happens with with ... assert ..., as shown by the following example (that Pulse fails to verify for the same reason):

fn test_with_assert_pure(r: R.ref nat)
    requires R.pts_to r full_perm 5 
    ensures R.pts_to r full_perm 5
{
    with v. assert (R.pts_to r full_perm v ** pure (v = 5));
    ()
}

[nikswamy]

This fails with "Impossible: instantiated abstraction is not an F* term"

fn trivial (x:unit)
requires emp
ensures emp
{
  assert (pure (5 == 5));
  ()
}

Whereas this succeeds:

fn trivial (x:unit)
requires emp
ensures emp
{
  assert_ (pure (5 == 5));
  ()
}

and so does this:

fn test_with_assert_pure(r: R.ref nat)
    requires R.pts_to r full_perm 5 
    ensures R.pts_to r full_perm 5
{
    with v. assert (R.pts_to r full_perm v ** pure (v = 5));
    ()
}