val inverses16 (u:unit) : Lemma (DV.inverses get16 put16)
val inverses16 (u:unit) : Lemma (DV.inverses get16 put16)
let inverses16 (u:unit) =
  get16_reveal ();
  put16_reveal ();
  let aux (x:Seq.lseq U8.t 2) : Lemma (put16 (get16 x) == x) =
    assert (Seq.equal x (put16 (get16 x)))
  in Classical.forall_intro aux
module Vale.Interop.Views
open FStar.Mul

let inverses8 (u:unit) =
  get8_reveal ();
  put8_reveal ();
  let aux (x:Seq.lseq U8.t 1) : Lemma (put8 (get8 x) == x) =
    assert (Seq.equal x (put8 (get8 x)))
  in Classical.forall_intro aux
/
Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.Interop.Views.fst
u32: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures LowStar.BufferView.Down.inverses Vale.Interop.Views.get16 Vale.Interop.Views.put16)
Prims.unit FStar.Classical.forall_intro FStar.Seq.Properties.lseq FStar.UInt8.t Prims.eq2 Vale.Interop.Views.put16 Vale.Interop.Views.get16 Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims._assert FStar.Seq.Base.equal Vale.Interop.Views.put16_reveal Vale.Interop.Views.get16_reveal
let inverses16 (u: unit) =
  
get16_reveal ();
put16_reveal ();
let aux (x: Seq.lseq U8.t 2) : Lemma (put16 (get16 x) == x) =
  assert (Seq.equal x (put16 (get16 x)))
in
Classical.forall_intro aux