val vptr0_rewrite
      (#a: Type)
      (r: ref a)
      (p: perm)
      (s: normal (vrefine_t (A.varrayp r p) (vptr0_refine r)))
    : Tot a
let vptr0_rewrite
  (#a: Type)
  (r: ref a)
  (p: perm)
  (s: normal (vrefine_t (A.varrayp r p) (vptr0_refine r)))
: Tot a
= Seq.index s 0
val vptr0_rewrite
      (#a: Type)
      (r: ref a)
      (p: perm)
      (s: normal (vrefine_t (A.varrayp r p) (vptr0_refine r)))
    : Tot a
let vptr0_rewrite
      (#a: Type)
      (r: ref a)
      (p: perm)
      (s: normal (vrefine_t (A.varrayp r p) (vptr0_refine r)))
    : Tot a =
Seq.index s 0
Steel.ArrayRef.fst.checked
Steel.Array.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Steel.ArrayRef.fst
Steel.ArrayRef.ref Steel.FractionalPermission.perm Steel.Effect.Common.normal Steel.Effect.Common.vrefine_t Steel.Array.varrayp Steel.ArrayRef.vptr0_refine FStar.Seq.Base.index
module Steel.ArrayRef

module A = Steel.Array

let null #a = A.null #a

let is_null r = A.is_null r

let vptr0_refine
  (#a: Type0)
  (r: ref a)
  (s: Seq.lseq a (A.length r))
: Tot prop
= Seq.length s == 1

let vptr0_rewrite
  (#a: Type)
  (r: ref a)
  (p: perm)
  (s: normal (vrefine_t (A.varrayp r p) (vptr0_refine r)))
val vptr0_rewrite
      (#a: Type)
      (r: ref a)
      (p: perm)
      (s: normal (vrefine_t (A.varrayp r p) (vptr0_refine r)))
    : Tot a

    r: Steel.ArrayRef.ref a ->
    p: Steel.FractionalPermission.perm ->
    s:
      Steel.Effect.Common.normal (Steel.Effect.Common.vrefine_t (Steel.Array.varrayp r p)
            (Steel.ArrayRef.vptr0_refine r))
  -> a