pure in assert_ does not work (Pulse) about steel HOT 1 CLOSED

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

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

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));
    ()
}