val inverses32 (u:unit) : Lemma (DV.inverses get32 put32)
let inverses32 (u:unit) =
  get32_reveal ();
  put32_reveal ();
  Classical.forall_intro (four_to_seq_to_four_LE #nat8);
  Classical.forall_intro (seq_to_four_to_seq_LE #nat8)
val inverses32 (u:unit) : Lemma (DV.inverses get32 put32)
let inverses32 (u: unit) =
get32_reveal ();
put32_reveal ();
Classical.forall_intro (four_to_seq_to_four_LE #nat8);
Classical.forall_intro (seq_to_four_to_seq_LE #nat8)
Vale.Interop.Views.fst.checked
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
Prims.unit FStar.Classical.forall_intro Vale.Def.Words_s.four Vale.Def.Types_s.nat8 Prims.eq2 Vale.Def.Words.Seq_s.seq_to_four_LE Vale.Def.Words.Seq_s.four_to_seq_LE Vale.Def.Words.Seq.seq_to_four_to_seq_LE Vale.Def.Words.Seq_s.seq4 Vale.Def.Words.Seq.four_to_seq_to_four_LE Vale.Interop.Views.put32_reveal Vale.Interop.Views.get32_reveal
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

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

#set-options "--z3rlimit 40"
val inverses32 (u:unit) : Lemma (DV.inverses get32 put32)
u21: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures LowStar.BufferView.Down.inverses Vale.Interop.Views.get32 Vale.Interop.Views.put32)