val aliasKeyTBS_payload_t' : Type0
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
)
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 = ()
/
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
Type0
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
let aliasKeyTBS_payload_t' =
  
(((((((x509_version_t `tuple2` x509_serialNumber_t) `tuple2` algorithmIdentifier_t)
          `tuple2`
          aliasKeyTBS_issuer_t)
        `tuple2`
        x509_validity_t)
      `tuple2`
      aliasKeyTBS_subject_t)
    `tuple2`
    subjectPublicKeyInfo_t)
  `tuple2`
  (x509_extensions_t_inbound serialize_aliasKeyTBS_extensions))