val synth_aliasKeyTBS_payload_t' (x: aliasKeyTBS_payload_t)
    : Tot (x': aliasKeyTBS_payload_t'{x == synth_aliasKeyTBS_payload_t x'})
val synth_aliasKeyTBS_payload_t' (x: aliasKeyTBS_payload_t)
    : Tot (x': aliasKeyTBS_payload_t'{x == synth_aliasKeyTBS_payload_t x'})
let synth_aliasKeyTBS_payload_t'
  (x: aliasKeyTBS_payload_t)
: Tot (x': aliasKeyTBS_payload_t' { x == synth_aliasKeyTBS_payload_t x' })
= ((((((x.aliasKeyTBS_version,
        x.aliasKeyTBS_serialNumber),
        x.aliasKeyTBS_signatureAlg),
        x.aliasKeyTBS_issuer),
        x.aliasKeyTBS_validity),
        x.aliasKeyTBS_subject),
        x.aliasKeyTBS_aliasKey_pub),
        x.aliasKeyTBS_extensions
module L0.X509.AliasKeyTBS

open ASN1.Spec
open ASN1.Low
open X509
open L0.X509.AliasKeyTBS.Issuer
open L0.X509.AliasKeyTBS.Subject
open L0.X509.AliasKeyTBS.Extensions
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_payload_t' = (
(*
//  *       version         [0]  EXPLICIT Version DEFAULT v1,
//  *)
  x509_version_t `tuple2`
(*
//  *       serialNumber         CertificateSerialNumber,
//  *)
  x509_serialNumber_t `tuple2`
(*
//  *       signature            AlgorithmIdentifier,
//  *)
  algorithmIdentifier_t `tuple2`
(*
//  *       issuer               Name,
//  *)
  aliasKeyTBS_issuer_t `tuple2`
(*
//  *       validity             Validity,
//  *)
  x509_validity_t `tuple2`
(*
//  *       subject              Name,
//  *)
  aliasKeyTBS_subject_t `tuple2`
(*
//  *      subjectPublicKeyInfo SubjectPublicKeyInfo
//  *)
  subjectPublicKeyInfo_t `tuple2`
(*
//  *      extensions      [3]  EXPLICIT Extensions OPTIONAL
//  *)
  x509_extensions_t_inbound serialize_aliasKeyTBS_extensions
)

let synth_aliasKeyTBS_payload_t
  (x': aliasKeyTBS_payload_t')
: GTot (aliasKeyTBS_payload_t)
= { aliasKeyTBS_version      = fst (fst (fst (fst (fst (fst (fst x'))))));
    aliasKeyTBS_serialNumber = snd (fst (fst (fst (fst (fst (fst x'))))));
    aliasKeyTBS_signatureAlg = snd (fst (fst (fst (fst (fst x')))));
    aliasKeyTBS_issuer       = snd (fst (fst (fst (fst x'))));
    aliasKeyTBS_validity     = snd (fst (fst (fst x')));
    aliasKeyTBS_subject      = snd (fst (fst x'));
    aliasKeyTBS_aliasKey_pub = snd (fst x');
    aliasKeyTBS_extensions   = snd x' }
/
X509.fst.checked prims.fst.checked L0.X509.AliasKeyTBS.Subject.fsti.checked L0.X509.AliasKeyTBS.Issuer.fsti.checked L0.X509.AliasKeyTBS.Extensions.fsti.checked FStar.Seq.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.fst
x: L0.X509.AliasKeyTBS.aliasKeyTBS_payload_t
  -> x':
    L0.X509.AliasKeyTBS.aliasKeyTBS_payload_t'
      {x == L0.X509.AliasKeyTBS.synth_aliasKeyTBS_payload_t x'}
L0.X509.AliasKeyTBS.aliasKeyTBS_payload_t FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.tuple2 X509.BasicFields.Version.x509_version_t X509.BasicFields.SerialNumber.x509_serialNumber_t X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_t X509.BasicFields.Validity.x509_validity_t L0.X509.AliasKeyTBS.Subject.aliasKeyTBS_subject_t X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t X509.BasicFields.Extensions.x509_extensions_t_inbound ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE L0.X509.AliasKeyTBS.Extensions.aliasKeyTBS_extensions_t L0.X509.AliasKeyTBS.Extensions.parse_aliasKeyTBS_extensions L0.X509.AliasKeyTBS.Extensions.serialize_aliasKeyTBS_extensions L0.X509.AliasKeyTBS.__proj__MkaliasKeyTBS_payload_t__item__aliasKeyTBS_version L0.X509.AliasKeyTBS.__proj__MkaliasKeyTBS_payload_t__item__aliasKeyTBS_serialNumber L0.X509.AliasKeyTBS.__proj__MkaliasKeyTBS_payload_t__item__aliasKeyTBS_signatureAlg L0.X509.AliasKeyTBS.__proj__MkaliasKeyTBS_payload_t__item__aliasKeyTBS_issuer L0.X509.AliasKeyTBS.__proj__MkaliasKeyTBS_payload_t__item__aliasKeyTBS_validity L0.X509.AliasKeyTBS.__proj__MkaliasKeyTBS_payload_t__item__aliasKeyTBS_subject L0.X509.AliasKeyTBS.__proj__MkaliasKeyTBS_payload_t__item__aliasKeyTBS_aliasKey_pub L0.X509.AliasKeyTBS.__proj__MkaliasKeyTBS_payload_t__item__aliasKeyTBS_extensions L0.X509.AliasKeyTBS.aliasKeyTBS_payload_t' Prims.eq2 L0.X509.AliasKeyTBS.synth_aliasKeyTBS_payload_t
let synth_aliasKeyTBS_payload_t' (x: aliasKeyTBS_payload_t)
    : Tot (x': aliasKeyTBS_payload_t'{x == synth_aliasKeyTBS_payload_t x'}) =
  
((((((x.aliasKeyTBS_version, x.aliasKeyTBS_serialNumber), x.aliasKeyTBS_signatureAlg),
        x.aliasKeyTBS_issuer),
      x.aliasKeyTBS_validity),
    x.aliasKeyTBS_subject),
  x.aliasKeyTBS_aliasKey_pub),
x.aliasKeyTBS_extensions