val aliasKeyTBS_subject_payload_t' : Type0
let aliasKeyTBS_subject_payload_t' = (
  x509_RDN_x520_attribute_t COMMON_NAME  IA5_STRING `tuple2`
  x509_RDN_x520_attribute_t ORGANIZATION IA5_STRING `tuple2`
  x509_RDN_x520_attribute_t COUNTRY      PRINTABLE_STRING
)
module L0.X509.AliasKeyTBS.Subject

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

module B32 = FStar.Bytes

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

let decl = ()
/
X509.fst.checked prims.fst.checked FStar.Pervasives.Native.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.Subject.fst
Type0
FStar.Pervasives.Native.tuple2 X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_t X509.BasicFields.RelativeDistinguishedName.COMMON_NAME ASN1.Base.IA5_STRING X509.BasicFields.RelativeDistinguishedName.ORGANIZATION X509.BasicFields.RelativeDistinguishedName.COUNTRY ASN1.Base.PRINTABLE_STRING
let aliasKeyTBS_subject_payload_t' =
  
(((x509_RDN_x520_attribute_t COMMON_NAME IA5_STRING)
    `tuple2`
    (x509_RDN_x520_attribute_t ORGANIZATION IA5_STRING))
  `tuple2`
  (x509_RDN_x520_attribute_t COUNTRY PRINTABLE_STRING))