val lemma_serialize_asn1_sequence_TLV_size
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
  (x: inbound_sequence_value_of s)
: Lemma ( predicate_serialize_asn1_sequence_TLV_size s x )
val lemma_serialize_asn1_sequence_TLV_size
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
  (x: inbound_sequence_value_of s)
: Lemma ( predicate_serialize_asn1_sequence_TLV_size s x )
let lemma_serialize_asn1_sequence_TLV_size #k #t #p s x
= lemma_serialize_asn1_envelop_tag_with_TLV_size SEQUENCE s x
module ASN1.Spec.Value.SEQUENCE

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Spec.Value.Envelop

// let parse_asn1_sequence_TLV #k #t #p s
// = parse_asn1_envelop_tag_with_TLV SEQUENCE s

// let serialize_asn1_sequence_TLV #k #t #p s
// = serialize_asn1_envelop_tag_with_TLV SEQUENCE s

let lemma_serialize_asn1_sequence_TLV_unfold #k #t #p s x
= lemma_serialize_asn1_envelop_tag_with_TLV_unfold SEQUENCE s x
/
prims.fst.checked FStar.Pervasives.fsti.checked ASN1.Spec.Value.Envelop.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.SEQUENCE.fst
s: LowParse.Spec.Base.serializer p -> x: ASN1.Spec.Value.SEQUENCE.inbound_sequence_value_of s
  -> FStar.Pervasives.Lemma
    (ensures ASN1.Spec.Value.SEQUENCE.predicate_serialize_asn1_sequence_TLV_size s x)
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer ASN1.Spec.Value.SEQUENCE.inbound_sequence_value_of ASN1.Spec.Value.Envelop.lemma_serialize_asn1_envelop_tag_with_TLV_size ASN1.Base.SEQUENCE Prims.unit
let lemma_serialize_asn1_sequence_TLV_size #k #t #p s x =
  
lemma_serialize_asn1_envelop_tag_with_TLV_size SEQUENCE s x