val llu8 : l: ASN1.Base.asn1_value_length_of_type ASN1.Base.OID -> Type0
let llu8
  (l: asn1_value_length_of_type OID )
= List.llist UInt8.t l
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

unfold 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) }
/
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
l: ASN1.Base.asn1_value_length_of_type ASN1.Base.OID -> Type0
ASN1.Base.asn1_value_length_of_type ASN1.Base.OID FStar.List.Tot.Properties.llist FStar.UInt8.t
let llu8 (l: asn1_value_length_of_type OID) =
  
List.llist UInt8.t l