val filter_subjectPublicKeyInfo_payload_t'
      (x: (algorithmIdentifier_t) `tuple2` (datatype_of_asn1_type BIT_STRING))
    : GTot bool
val filter_subjectPublicKeyInfo_payload_t'
      (x: (algorithmIdentifier_t) `tuple2` (datatype_of_asn1_type BIT_STRING))
    : GTot bool
let filter_subjectPublicKeyInfo_payload_t'
  (x: (algorithmIdentifier_t) `tuple2` (datatype_of_asn1_type BIT_STRING))
: GTot bool
= (snd x).bs_len = 33ul &&
  (snd x).bs_unused_bits = 0ul
module X509.BasicFields.SubjectPublicKeyInfo
open ASN1.Spec
open ASN1.Low

open X509.Base
open X509.Crypto

open FStar.Integers

#set-options "--fuel 0 --ifuel 0"
/
X509.Crypto.fst.checked X509.Base.fst.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.SubjectPublicKeyInfo.fst

    x:
      (X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t *
        ASN1.Base.datatype_of_asn1_type ASN1.Base.BIT_STRING)
  -> Prims.GTot Prims.bool
FStar.Pervasives.Native.tuple2 X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t ASN1.Base.datatype_of_asn1_type ASN1.Base.BIT_STRING Prims.op_AmpAmp Prims.op_Equality FStar.UInt32.t ASN1.Base.__proj__Mkbit_string_t__item__bs_len FStar.Pervasives.Native.snd FStar.UInt32.__uint_to_t ASN1.Base.__proj__Mkbit_string_t__item__bs_unused_bits Prims.bool
let filter_subjectPublicKeyInfo_payload_t'
      (x: (algorithmIdentifier_t) `tuple2` (datatype_of_asn1_type BIT_STRING))
    : GTot bool =
  
(snd x).bs_len = 33ul && (snd x).bs_unused_bits = 0ul