val lemma_serialize_aliasKeyTBS_subject_payload_unfold
  (x: aliasKeyTBS_subject_payload_t)
: Lemma (
  serialize_aliasKeyTBS_subject_payload `serialize` x ==
 (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING `serialize` x.aliasKeyTBS_subject_Common)
  `Seq.append`
 (serialize_RDN_x520_attribute ORGANIZATION IA5_STRING `serialize` x.aliasKeyTBS_subject_Organization)
  `Seq.append`
 (serialize_RDN_x520_attribute COUNTRY PRINTABLE_STRING `serialize` x.aliasKeyTBS_subject_Country)
)
val lemma_serialize_aliasKeyTBS_subject_payload_unfold
  (x: aliasKeyTBS_subject_payload_t)
: Lemma (
  serialize_aliasKeyTBS_subject_payload `serialize` x ==
 (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING `serialize` x.aliasKeyTBS_subject_Common)
  `Seq.append`
 (serialize_RDN_x520_attribute ORGANIZATION IA5_STRING `serialize` x.aliasKeyTBS_subject_Organization)
  `Seq.append`
 (serialize_RDN_x520_attribute COUNTRY PRINTABLE_STRING `serialize` x.aliasKeyTBS_subject_Country)
)
let lemma_serialize_aliasKeyTBS_subject_payload_unfold x
= serialize_nondep_then_eq
  (* s1 *) (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING)
  (* s2 *) (serialize_RDN_x520_attribute ORGANIZATION IA5_STRING)
  (* in *) (fst (synth_aliasKeyTBS_subject_payload_t' x));
  serialize_nondep_then_eq
  (* s1 *) (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute ORGANIZATION IA5_STRING)
  (* s2 *) (serialize_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* in *) (synth_aliasKeyTBS_subject_payload_t' x);
  serialize_synth_eq
  (* p1 *) (parse_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `nondep_then`
            parse_RDN_x520_attribute ORGANIZATION IA5_STRING
            `nondep_then`
            parse_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* f2 *) (synth_aliasKeyTBS_subject_payload_t)
  (* s1 *) (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute ORGANIZATION IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* g1 *) (synth_aliasKeyTBS_subject_payload_t')
  (* prf*) ()
  (* in *) (x)
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 = ()

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
)

let synth_aliasKeyTBS_subject_payload_t
  (x': aliasKeyTBS_subject_payload_t')
: GTot (aliasKeyTBS_subject_payload_t)
= { aliasKeyTBS_subject_Common       = fst (fst x');
    aliasKeyTBS_subject_Organization = snd (fst x');
    aliasKeyTBS_subject_Country      = snd x' }

inline_for_extraction noextract
let synth_aliasKeyTBS_subject_payload_t'
  (x: aliasKeyTBS_subject_payload_t)
: Tot (x': aliasKeyTBS_subject_payload_t'
           { x == synth_aliasKeyTBS_subject_payload_t x' })
= (x.aliasKeyTBS_subject_Common,
   x.aliasKeyTBS_subject_Organization),
   x.aliasKeyTBS_subject_Country

let parse_aliasKeyTBS_subject_payload
= parse_RDN_x520_attribute COMMON_NAME  IA5_STRING
  `nondep_then`
  parse_RDN_x520_attribute ORGANIZATION IA5_STRING
  `nondep_then`
  parse_RDN_x520_attribute COUNTRY      PRINTABLE_STRING
  `parse_synth`
  synth_aliasKeyTBS_subject_payload_t

let serialize_aliasKeyTBS_subject_payload
= serialize_synth
  (* p1 *) (parse_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `nondep_then`
            parse_RDN_x520_attribute ORGANIZATION IA5_STRING
            `nondep_then`
            parse_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* f2 *) (synth_aliasKeyTBS_subject_payload_t)
  (* s1 *) (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute ORGANIZATION IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* g1 *) (synth_aliasKeyTBS_subject_payload_t')
  (* prf*) ()
/
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
x: L0.X509.AliasKeyTBS.Subject.aliasKeyTBS_subject_payload_t
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serialize L0.X509.AliasKeyTBS.Subject.serialize_aliasKeyTBS_subject_payload
        x ==
      FStar.Seq.Base.append (FStar.Seq.Base.append (LowParse.Spec.Base.serialize (X509.BasicFields.RelativeDistinguishedName.serialize_RDN_x520_attribute
                    X509.BasicFields.RelativeDistinguishedName.COMMON_NAME
                    ASN1.Base.IA5_STRING)
                (MkaliasKeyTBS_subject_payload_t?.aliasKeyTBS_subject_Common x))
            (LowParse.Spec.Base.serialize (X509.BasicFields.RelativeDistinguishedName.serialize_RDN_x520_attribute
                    X509.BasicFields.RelativeDistinguishedName.ORGANIZATION
                    ASN1.Base.IA5_STRING)
                (MkaliasKeyTBS_subject_payload_t?.aliasKeyTBS_subject_Organization x)))
        (LowParse.Spec.Base.serialize (X509.BasicFields.RelativeDistinguishedName.serialize_RDN_x520_attribute
                X509.BasicFields.RelativeDistinguishedName.COUNTRY
                ASN1.Base.PRINTABLE_STRING)
            (MkaliasKeyTBS_subject_payload_t?.aliasKeyTBS_subject_Country x)))
L0.X509.AliasKeyTBS.Subject.aliasKeyTBS_subject_payload_t LowParse.Spec.Combinators.serialize_synth_eq LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SET 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 LowParse.Spec.Combinators.nondep_then X509.BasicFields.RelativeDistinguishedName.parse_RDN_x520_attribute L0.X509.AliasKeyTBS.Subject.synth_aliasKeyTBS_subject_payload_t LowParse.Spec.Combinators.serialize_nondep_then X509.BasicFields.RelativeDistinguishedName.serialize_RDN_x520_attribute L0.X509.AliasKeyTBS.Subject.synth_aliasKeyTBS_subject_payload_t' Prims.unit LowParse.Spec.Combinators.serialize_nondep_then_eq FStar.Pervasives.Native.fst
let lemma_serialize_aliasKeyTBS_subject_payload_unfold x =
  
serialize_nondep_then_eq (serialize_RDN_x520_attribute COMMON_NAME IA5_STRING)
  (serialize_RDN_x520_attribute ORGANIZATION IA5_STRING)
  (fst (synth_aliasKeyTBS_subject_payload_t' x));
serialize_nondep_then_eq ((serialize_RDN_x520_attribute COMMON_NAME IA5_STRING)
    `serialize_nondep_then`
    (serialize_RDN_x520_attribute ORGANIZATION IA5_STRING))
  (serialize_RDN_x520_attribute COUNTRY PRINTABLE_STRING)
  (synth_aliasKeyTBS_subject_payload_t' x);
serialize_synth_eq (((parse_RDN_x520_attribute COMMON_NAME IA5_STRING)
      `nondep_then`
      (parse_RDN_x520_attribute ORGANIZATION IA5_STRING))
    `nondep_then`
    (parse_RDN_x520_attribute COUNTRY PRINTABLE_STRING))
  (synth_aliasKeyTBS_subject_payload_t)
  (((serialize_RDN_x520_attribute COMMON_NAME IA5_STRING)
      `serialize_nondep_then`
      (serialize_RDN_x520_attribute ORGANIZATION IA5_STRING))
    `serialize_nondep_then`
    (serialize_RDN_x520_attribute COUNTRY PRINTABLE_STRING))
  (synth_aliasKeyTBS_subject_payload_t')
  ()
  (x)