val clens_certificate13_certificate_request_context:LL.clens certificate13
  certificate13_certificate_request_context
val clens_certificate13_certificate_request_context:LL.clens certificate13
  certificate13_certificate_request_context
let clens_certificate13_certificate_request_context : LL.clens certificate13 certificate13_certificate_request_context = {
  LL.clens_cond = (fun _ -> True);
  LL.clens_get = (fun x -> x.certificate_request_context);
}
module MiTLS.Parsers.Certificate13

(* This file has been automatically generated by EverParse. *)
open FStar.Bytes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module LP = LowParse.Spec.Base
module LS = LowParse.SLow.Base
module LSZ = LowParse.SLow.Base
module LPI = LowParse.Spec.AllIntegers
module LL = LowParse.Low.Base
module L = FStar.List.Tot
module B = LowStar.Buffer
module BY = FStar.Bytes
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

open MiTLS.Parsers.CertificateEntry13

(* Type of field certificate_request_context*)
include MiTLS.Parsers.Certificate13_certificate_request_context

(* Type of field certificate_list*)
include MiTLS.Parsers.Certificate13_certificate_list

type certificate13 = {
  certificate_request_context : certificate13_certificate_request_context;
  certificate_list : certificate13_certificate_list;
}

inline_for_extraction noextract let certificate13_parser_kind = LP.strong_parser_kind 4 16777474 None

noextract val certificate13_parser: LP.parser certificate13_parser_kind certificate13

noextract val certificate13_serializer: LP.serializer certificate13_parser

noextract val certificate13_bytesize (x:certificate13) : GTot nat

noextract val certificate13_bytesize_eq (x:certificate13) : Lemma (certificate13_bytesize x == Seq.length (LP.serialize certificate13_serializer x))

val certificate13_parser32: LS.parser32 certificate13_parser

val certificate13_serializer32: LS.serializer32 certificate13_serializer

val certificate13_size32: LSZ.size32 certificate13_serializer

val certificate13_validator: LL.validator certificate13_parser

val certificate13_jumper: LL.jumper certificate13_parser

val certificate13_bytesize_eqn (x: certificate13) : Lemma (certificate13_bytesize x == (certificate13_certificate_request_context_bytesize (x.certificate_request_context)) + (certificate13_certificate_list_bytesize (x.certificate_list))) [SMTPat (certificate13_bytesize x)]
/
prims.fst.checked MiTLS.Parsers.CertificateEntry13.fsti.checked MiTLS.Parsers.Certificate13_certificate_request_context.fsti.checked MiTLS.Parsers.Certificate13_certificate_list.fsti.checked LowStar.Buffer.fst.checked LowParse.Spec.Base.fsti.checked LowParse.Spec.AllIntegers.fst.checked LowParse.SLow.Base.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.Parsers.Certificate13.fsti
LowParse.Low.Base.Spec.clens MiTLS.Parsers.Certificate13.certificate13
  MiTLS.Parsers.Certificate13_certificate_request_context.certificate13_certificate_request_context
LowParse.Low.Base.Spec.Mkclens MiTLS.Parsers.Certificate13.certificate13 MiTLS.Parsers.Certificate13_certificate_request_context.certificate13_certificate_request_context Prims.l_True MiTLS.Parsers.Certificate13.__proj__Mkcertificate13__item__certificate_request_context
let clens_certificate13_certificate_request_context:LL.clens certificate13
  certificate13_certificate_request_context =
  
{ LL.clens_cond = (fun _ -> True); LL.clens_get = (fun x -> x.certificate_request_context) }