Function lemma_pte_index_bound 

pub proof fn lemma_pte_index_bound<C: PagingConstsTrait>(
    va: Vaddr,
    level: PagingLevel,
)

requires

1 <= level <= C::NR_LEVELS(),

ensures

pte_index_spec::<C>(va, level) < nr_subpage_per_huge::<C>(),

Every extracted index is in the configured fanout.