Function asn1_starts_disjoint 

pub open spec fn asn1_starts_disjoint(
    left: Asn1StartDomain,
    right: Asn1StartDomain,
) -> bool

{
    &&& !(left.accepts_empty && right.accepts_empty)
    &&& tag_lead_masks_disjoint(left.tags, right.tags)

}

A constant-size, quantifier-free sufficient test for disjoint ASN.1 FIRST domains.