val parse_aliasKeyTBS_issuer_payload_kind:parser_kind
val parse_aliasKeyTBS_issuer_payload_kind:parser_kind
let parse_aliasKeyTBS_issuer_payload_kind
: parser_kind
= parse_asn1_envelop_tag_with_TLV_kind SET
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SET
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SET
module L0.X509.AliasKeyTBS.Issuer

open ASN1.Spec
open ASN1.Low
open X509
open FStar.Integers

open L0.X509.LengthUtils

module B32 = FStar.Bytes

#set-options "--z3rlimit 128 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

val decl : unit

noeq
type aliasKeyTBS_issuer_payload_t = {
  aliasKeyTBS_issuer_Common      : x509_RDN_x520_attribute_t COMMON_NAME  IA5_STRING;
  aliasKeyTBS_issuer_Organization: x509_RDN_x520_attribute_t ORGANIZATION IA5_STRING;
  aliasKeyTBS_issuer_Country     : x509_RDN_x520_attribute_t COUNTRY      PRINTABLE_STRING
}
/
X509.fst.checked prims.fst.checked L0.X509.LengthUtils.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
L0.X509.AliasKeyTBS.Issuer.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SET
let parse_aliasKeyTBS_issuer_payload_kind:parser_kind =
  
((parse_asn1_envelop_tag_with_TLV_kind SET)
  `and_then_kind`
  (parse_asn1_envelop_tag_with_TLV_kind SET))
`and_then_kind`
(parse_asn1_envelop_tag_with_TLV_kind SET)