Function asn1_start_identity_uint 

pub open spec fn asn1_start_identity_uint(class: Class, number: u64) -> Asn1StartDomain

{
    asn1_start_union(
        asn1_start_exact_uint(class, false, number),
        asn1_start_exact_uint(class, true, number),
    )
}

FIRST certificate for either constructed bit of a numeric tag.