Function tag_lead_index 

pub open spec fn tag_lead_index(tag: Tag) -> u64

{
    let low = tag_lead_low(tag.number);
    if tag.constructed { low | 32u64 } else { low }
}