val lemma_dv_equal
      (#src: Type)
      (#rel #rrel: MB.srel src)
      (#dst: Type)
      (view: DV.view src dst)
      (b: MB.mbuffer src rel rrel)
      (h0 h1: HS.mem)
    : Lemma (requires MB.as_seq h0 b == MB.as_seq h1 b)
      (ensures
        (let dv = DV.mk_buffer_view b view in
          DV.as_seq h0 dv == DV.as_seq h1 dv))
let lemma_dv_equal
  (#src:Type)
  (#rel #rrel:MB.srel src)
  (#dst:Type)
  (view:DV.view src dst)
  (b:MB.mbuffer src rel rrel)
  (h0 h1:HS.mem) : Lemma
  (requires MB.as_seq h0 b == MB.as_seq h1 b)
  (ensures (let dv = DV.mk_buffer_view b view in
    DV.as_seq h0 dv == DV.as_seq h1 dv)) =
    let dv = DV.mk_buffer_view b view in
    let s0 = DV.as_seq h0 dv in
    let s1 = DV.as_seq h1 dv in
    let aux (i:nat{i < DV.length dv}) : Lemma (Seq.index s0 i == Seq.index s1 i) =
      DV.as_seq_sel h0 dv i;
      DV.as_seq_sel h1 dv i;
      DV.get_sel h0 dv i;
      DV.get_sel h1 dv i
    in Classical.forall_intro aux;
    Seq.lemma_eq_intro s0 s1
val lemma_dv_equal
      (#src: Type)
      (#rel #rrel: MB.srel src)
      (#dst: Type)
      (view: DV.view src dst)
      (b: MB.mbuffer src rel rrel)
      (h0 h1: HS.mem)
    : Lemma (requires MB.as_seq h0 b == MB.as_seq h1 b)
      (ensures
        (let dv = DV.mk_buffer_view b view in
          DV.as_seq h0 dv == DV.as_seq h1 dv))
let lemma_dv_equal
      (#src: Type)
      (#rel #rrel: MB.srel src)
      (#dst: Type)
      (view: DV.view src dst)
      (b: MB.mbuffer src rel rrel)
      (h0 h1: HS.mem)
    : Lemma (requires MB.as_seq h0 b == MB.as_seq h1 b)
      (ensures
        (let dv = DV.mk_buffer_view b view in
          DV.as_seq h0 dv == DV.as_seq h1 dv)) =
let dv = DV.mk_buffer_view b view in
let s0 = DV.as_seq h0 dv in
let s1 = DV.as_seq h1 dv in
let aux (i: nat{i < DV.length dv}) : Lemma (Seq.index s0 i == Seq.index s1 i) =
  DV.as_seq_sel h0 dv i;
  DV.as_seq_sel h1 dv i;
  DV.get_sel h0 dv i;
  DV.get_sel h1 dv i
in
Classical.forall_intro aux;
Seq.lemma_eq_intro s0 s1
Vale.Lib.BufferViewHelpers.fst.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.ModifiesPat.fst.checked LowStar.Modifies.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.BufferView.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
Vale.Lib.BufferViewHelpers.fst
LowStar.Monotonic.Buffer.srel LowStar.BufferView.Down.view LowStar.Monotonic.Buffer.mbuffer FStar.Monotonic.HyperStack.mem FStar.Seq.Base.lemma_eq_intro Prims.unit FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan LowStar.BufferView.Down.length Prims.eq2 FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern LowStar.BufferView.Down.get_sel LowStar.BufferView.Down.as_seq_sel FStar.Seq.Properties.lseq LowStar.BufferView.Down.as_seq LowStar.BufferView.Down.buffer LowStar.BufferView.Down.mk_buffer_view FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq
module Vale.Lib.BufferViewHelpers
open FStar.Mul

module MB = LowStar.Monotonic.Buffer
module BV = LowStar.BufferView
module DV = LowStar.BufferView.Down
module UV = LowStar.BufferView.Up
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
open FStar.HyperStack.ST

open LowStar.Modifies
open LowStar.ModifiesPat

let lemma_dv_equal
  (#src:Type)
  (#rel #rrel:MB.srel src)
  (#dst:Type)
  (view:DV.view src dst)
  (b:MB.mbuffer src rel rrel)
  (h0 h1:HS.mem) : Lemma
  (requires MB.as_seq h0 b == MB.as_seq h1 b)
val lemma_dv_equal
      (#src: Type)
      (#rel #rrel: MB.srel src)
      (#dst: Type)
      (view: DV.view src dst)
      (b: MB.mbuffer src rel rrel)
      (h0 h1: HS.mem)
    : Lemma (requires MB.as_seq h0 b == MB.as_seq h1 b)
      (ensures
        (let dv = DV.mk_buffer_view b view in
          DV.as_seq h0 dv == DV.as_seq h1 dv))

    view: LowStar.BufferView.Down.view src dst ->
    b: LowStar.Monotonic.Buffer.mbuffer src rel rrel ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires LowStar.Monotonic.Buffer.as_seq h0 b == LowStar.Monotonic.Buffer.as_seq h1 b)
      (ensures
        (let dv = LowStar.BufferView.Down.mk_buffer_view b view in
          LowStar.BufferView.Down.as_seq h0 dv == LowStar.BufferView.Down.as_seq h1 dv))