Function lemma_asn1_starts_disjoint_exact 

pub broadcast proof fn lemma_asn1_starts_disjoint_exact(left: Tag, right: Tag)

ensures

#[trigger] asn1_starts_disjoint(asn1_start_exact(left), asn1_start_exact(right))
    <==> tag_leads_distinct(left, right),

Exact one-octet FIRST domains are disjoint exactly when their leading octets differ.