You understood the notation. So "nat64" cleared up two notation deficiencies: correct base type, and explicit declaration of modularity. A plain natural (unbo

You understood the notation. So "nat64" cleared up two notation deficiencies: correct base type, and explicit declaration of modularity. A plain natural (unbounded/big) would be "nat" or "natural".