val reveal_pts_to
  (#a: _) (r: ref a) (p: perm) (x: a)
: Lemma
  (pts_to r p x `equiv` Steel.ST.HigherReference.pts_to (reveal_ref r) p x)
let reveal_pts_to r p x =
  equiv_refl (Steel.ST.HigherReference.pts_to (reveal_ref r) p x)
val reveal_pts_to
  (#a: _) (r: ref a) (p: perm) (x: a)
: Lemma
  (pts_to r p x `equiv` Steel.ST.HigherReference.pts_to (reveal_ref r) p x)
let reveal_pts_to r p x =
equiv_refl (Steel.ST.HigherReference.pts_to (reveal_ref r) p x)
Steel.ST.GhostHigherReference.fst.checked
Steel.ST.HigherReference.fst.checked Steel.ST.Coercions.fsti.checked Steel.HigherReference.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.GhostHigherReference.fst
Steel.ST.GhostHigherReference.ref Steel.FractionalPermission.perm Steel.Effect.Common.equiv_refl Steel.ST.HigherReference.pts_to Steel.ST.GhostHigherReference.reveal_ref Prims.unit
module Steel.ST.GhostHigherReference

// needed because I need to know that `Steel.ST.HigherReference.ref a`
// can be turned into `Steel.HigherReference.ref a`
friend Steel.ST.HigherReference

module RST = Steel.ST.HigherReference
module R = Steel.HigherReference

module STC = Steel.ST.Coercions

// FIXME: WHY WHY WHY in `Ghost.reveal (ref a)` is `a` not strictly positive?

[@@erasable]
noeq
type ref' ([@@@strictly_positive] a : Type u#1) : Type0
= | Hide: (reveal: R.ref a) -> ref' a

let ref a = ref' a

let pts_to r p v = RST.pts_to r.reveal p v

let reveal_ref r = r.reveal

let hide_ref r = Hide r

let hide_reveal_ref r = ()
val reveal_pts_to
  (#a: _) (r: ref a) (p: perm) (x: a)
: Lemma
  (pts_to r p x `equiv` Steel.ST.HigherReference.pts_to (reveal_ref r) p x)
r: Steel.ST.GhostHigherReference.ref a -> p: Steel.FractionalPermission.perm -> x: a
  -> FStar.Pervasives.Lemma
    (ensures
      Steel.Effect.Common.equiv (Steel.ST.GhostHigherReference.pts_to r p x)
        (Steel.ST.HigherReference.pts_to (Steel.ST.GhostHigherReference.reveal_ref r) p x))