Function lemma_asn1_starts_disjoint_exact_uint 

pub broadcast proof fn lemma_asn1_starts_disjoint_exact_uint(
    left_class: Class,
    left_constructed: bool,
    left_number: u64,
    right_class: Class,
    right_constructed: bool,
    right_number: u64,
)

ensures

#[trigger]
asn1_starts_disjoint(
    asn1_start_exact_uint(left_class, left_constructed, left_number),
    asn1_start_exact_uint(right_class, right_constructed, right_number),
)
    <==> tag_leads_distinct_uint(
        left_class,
        left_constructed,
        left_number,
        right_class,
        right_constructed,
        right_number,
    ),

Numeric singleton certificates are disjoint exactly when their lead octets differ.