val parse_seq_all_bytes_injective: Prims.unit -> Lemma (injective parse_seq_all_bytes')
val parse_seq_all_bytes_injective: Prims.unit -> Lemma (injective parse_seq_all_bytes')
let parse_seq_all_bytes_injective () : Lemma
  (injective parse_seq_all_bytes')
= let prf
    (b1 b2: bytes)
  : Lemma
    (requires (injective_precond parse_seq_all_bytes' b1 b2))
    (ensures (injective_postcond parse_seq_all_bytes' b1 b2))
  = ()
  in
  Classical.forall_intro_2 (fun x -> Classical.move_requires (prf x))
module LowParse.Spec.SeqBytes
include LowParse.Spec.SeqBytes.Base
include LowParse.Spec.VLData

module Seq = FStar.Seq
module U32 = FStar.UInt32

(* VLBytes *)

(* For the payload: since the input buffer is truncated at the time of
reading the length header, "parsing" the payload will always succeed,
by just returning it unchanged (unless the length of the input
is greater than 2^32) *)

let parse_seq_all_bytes_kind =
  {
    parser_kind_low = 0;
    parser_kind_high = None;
    parser_kind_metadata = None;
    parser_kind_subkind = Some ParserConsumesAll;
  }

let parse_seq_all_bytes'
  (input: bytes)
: GTot (option (bytes * consumed_length input))
= let len = Seq.length input in
    Some (input, len)

#set-options "--z3rlimit 16"
/
prims.fst.checked LowParse.Spec.VLData.fsti.checked LowParse.Spec.SeqBytes.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.SeqBytes.fst
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures LowParse.Spec.Base.injective LowParse.Spec.SeqBytes.parse_seq_all_bytes')
Prims.unit FStar.Classical.forall_intro_2 LowParse.Bytes.bytes Prims.l_imp LowParse.Spec.Base.injective_precond LowParse.Spec.SeqBytes.parse_seq_all_bytes' LowParse.Spec.Base.injective_postcond FStar.Classical.move_requires Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern LowParse.Spec.Base.injective
let parse_seq_all_bytes_injective () : Lemma (injective parse_seq_all_bytes') =
  
let prf (b1 b2: bytes)
    : Lemma (requires (injective_precond parse_seq_all_bytes' b1 b2))
      (ensures (injective_postcond parse_seq_all_bytes' b1 b2)) =
  ()
in
Classical.forall_intro_2 (fun x -> Classical.move_requires (prf x))