Function lemma_type_inv_range 

pub broadcast proof fn lemma_type_inv_range(cpu_id: CpuId)

requires

CpuId::type_inv(cpu_id),

ensures

0 <= cpu_id@ < cpu_count(),

Re-exposes the range fact of a CpuId beyond the closed type_inv.