val compositeDeviceID_payload_t' : Type0
let compositeDeviceID_payload_t'
= ((datatype_of_asn1_type INTEGER &
    subjectPublicKeyInfo_t) &
    fwid_t)
module L0.X509.CompositeDeviceID

open LowParse.Low.Base
open LowParse.Low.Combinators

open ASN1.Spec
open ASN1.Low

open X509.Base
open X509.BasicFields.SubjectPublicKeyInfo
open X509.Crypto
open L0.X509.Base
open L0.X509.FWID

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

let decl = ()

(* CompositeDeviceID *)
/
X509.Crypto.fst.checked X509.BasicFields.SubjectPublicKeyInfo.fsti.checked X509.Base.fst.checked prims.fst.checked LowParse.Low.Combinators.fsti.checked LowParse.Low.Base.fst.checked L0.X509.FWID.fsti.checked L0.X509.Base.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
L0.X509.CompositeDeviceID.fst
Type0
FStar.Pervasives.Native.tuple2 ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t L0.X509.FWID.fwid_t
let compositeDeviceID_payload_t' =
  
((datatype_of_asn1_type INTEGER & subjectPublicKeyInfo_t) & fwid_t)