Function tag_leads_distinct 

pub open spec fn tag_leads_distinct(left: Tag, right: Tag) -> bool

{
    ||| left.class != right.class
    ||| left.constructed != right.constructed
    ||| tag_lead_low(left.number) != tag_lead_low(right.number)

}

Whether two tags have different identifier leading octets.

All high tag numbers deliberately have index 31 within their primitive/constructed half, so this predicate preserves the documented conservative high-tag behavior.