pub proof fn lemma_oid_subidentifier_roundtrip(first: UInt, rest: Seq<UInt>)Expand description
ensures
oid_to_subidentifiers(oid_from_subidentifiers(first, rest)) == (first, rest),