Function lemma_oid_from_subidentifiers_wf 

pub proof fn lemma_oid_from_subidentifiers_wf(first: UInt, rest: Seq<UInt>)

ensures

oid_from_subidentifiers(first, rest).wf(),