Function lemma_oid_arcs_roundtrip 

pub proof fn lemma_oid_arcs_roundtrip(v: ObjectIdentifierSpec)

requires

v.wf(),

ensures

oid_from_subidentifiers(oid_first_subidentifier(v), v.rest) == v,