val vptr0_refine (#a: Type0) (r: ref a) (s: Seq.lseq a (A.length r)) : Tot prop
let vptr0_refine
  (#a: Type0)
  (r: ref a)
  (s: Seq.lseq a (A.length r))
: Tot prop
= Seq.length s == 1
val vptr0_refine (#a: Type0) (r: ref a) (s: Seq.lseq a (A.length r)) : Tot prop
let vptr0_refine (#a: Type0) (r: ref a) (s: Seq.lseq a (A.length r)) : Tot prop =
Seq.length s == 1
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 FStar.Seq.Properties.lseq Steel.ST.Array.length Prims.eq2 Prims.int FStar.Seq.Base.length Prims.prop
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))
val vptr0_refine (#a: Type0) (r: ref a) (s: Seq.lseq a (A.length r)) : Tot prop
r: Steel.ArrayRef.ref a -> s: FStar.Seq.Properties.lseq a (Steel.ST.Array.length r) -> Prims.prop