Function asn1_start_union 

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

{
    Asn1StartDomain {
        accepts_empty: left.accepts_empty || right.accepts_empty,
        tags: tag_lead_masks_union(left.tags, right.tags),
    }
}