val lu8 : Type0
let lu8
= l: list UInt8.t
  { asn1_length_inbound
      (List.length l)
      (asn1_value_length_min_of_type OID)
      (asn1_value_length_max_of_type OID) }
module ASN1.Spec.Value.OID

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open LowParse.Spec.SeqBytes.Base

open FStar.Integers

unfold noextract
let ( @ ) = List.Tot.Base.append
/
prims.fst.checked LowParse.Spec.SeqBytes.Base.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked FStar.List.fst.checked FStar.Integers.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.OID.fsti
Type0
Prims.list FStar.UInt8.t Prims.b2t ASN1.Base.asn1_length_inbound FStar.List.Tot.Base.length ASN1.Base.asn1_value_length_min_of_type ASN1.Base.OID ASN1.Base.asn1_value_length_max_of_type
let lu8 =
  
l:
list UInt8.t
  { asn1_length_inbound (List.length l)
      (asn1_value_length_min_of_type OID)
      (asn1_value_length_max_of_type OID) }