Normalization of `pts_to` makes an assertion fail (steel)

[aseemr]

The following fails, if we uncomment assert_spinoff then it succeeds. The reason is that pts_to gets reduced to Mk_vprop with lambdas as arguments, that end up getting different smt encoding:

module Test

open Steel.FractionalPermission
open Steel.Memory
open Steel.Effect
open Steel.Effect.Atomic
open Steel.Reference

assume val t : Type0

assume val f (x:t) : t

let test (#opened_invariants:_) (r:ref t) (x:t)
  : SteelGhostT unit opened_invariants
      (pts_to r full_perm (f x))
      (fun _ -> emp)

  = assume (f x == x);
    //assert_spinoff (pts_to r full_perm (f x) == pts_to r full_perm x);
    change_equal_slprop (pts_to r full_perm (f x)) (pts_to r full_perm x);
    sladmit ()

We discussed fixing it by making pts_to irreducible for the steel tactic. Similar examples exists for h_exists.