val x509_rdn_string_t : Type0
let x509_rdn_string_t = ASN1.Base.oid_t & ASN1.Base.character_string_t IA5_STRING
module L0.X509.DeviceIDCRI.Subject

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

open L0.X509.LengthUtils

module B32 = FStar.Bytes

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

val decl : unit
/
X509.fst.checked prims.fst.checked L0.X509.LengthUtils.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
L0.X509.DeviceIDCRI.Subject.fsti
Type0
FStar.Pervasives.Native.tuple2 ASN1.Base.oid_t ASN1.Base.character_string_t ASN1.Base.IA5_STRING
let x509_rdn_string_t =
  
ASN1.Base.oid_t & ASN1.Base.character_string_t IA5_STRING