Function oid_to_subidentifiers 

pub open spec fn oid_to_subidentifiers(v: ObjectIdentifierSpec) -> (UInt, Seq<UInt>)

{ (oid_first_subidentifier(v), v.rest) }