val synth_aliasKeyTBS_issuer_payload_t (x': aliasKeyTBS_issuer_payload_t')
    : GTot (aliasKeyTBS_issuer_payload_t)
val synth_aliasKeyTBS_issuer_payload_t (x': aliasKeyTBS_issuer_payload_t')
    : GTot (aliasKeyTBS_issuer_payload_t)
let synth_aliasKeyTBS_issuer_payload_t
  (x': aliasKeyTBS_issuer_payload_t')
: GTot (aliasKeyTBS_issuer_payload_t)
= { aliasKeyTBS_issuer_Common       = fst (fst x');
    aliasKeyTBS_issuer_Organization = snd (fst x');
    aliasKeyTBS_issuer_Country      = snd x' }
module L0.X509.AliasKeyTBS.Issuer

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 = ()

let aliasKeyTBS_issuer_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
)
/
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.Issuer.fst
x': L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_payload_t'
  -> Prims.GTot L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_payload_t
L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_payload_t' L0.X509.AliasKeyTBS.Issuer.MkaliasKeyTBS_issuer_payload_t FStar.Pervasives.Native.fst X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_t X509.BasicFields.RelativeDistinguishedName.COMMON_NAME ASN1.Base.IA5_STRING X509.BasicFields.RelativeDistinguishedName.ORGANIZATION FStar.Pervasives.Native.tuple2 X509.BasicFields.RelativeDistinguishedName.COUNTRY ASN1.Base.PRINTABLE_STRING FStar.Pervasives.Native.snd L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_payload_t
let synth_aliasKeyTBS_issuer_payload_t (x': aliasKeyTBS_issuer_payload_t')
    : GTot (aliasKeyTBS_issuer_payload_t) =
  
{
  aliasKeyTBS_issuer_Common = fst (fst x');
  aliasKeyTBS_issuer_Organization = snd (fst x');
  aliasKeyTBS_issuer_Country = snd x'
}