Function lemma_same_node_pte_indices_match 

pub proof fn lemma_same_node_pte_indices_match<C: PagingConstsTrait>(
    va1: Vaddr,
    va2: Vaddr,
    node_start: Vaddr,
    level: PagingLevel,
)

requires

level < C::NR_LEVELS(),

node_start <= va1,

va1 < node_start + page_size::<C>((level + 1) as PagingLevel),

node_start <= va2,

va2 < node_start + page_size::<C>((level + 1) as PagingLevel),

node_start as nat % page_size::<C>((level + 1) as PagingLevel) as nat == 0,

ensures

pte_index_spec::<C>(va1, (level + 1) as PagingLevel)
    == pte_index_spec::<C>(va2, (level + 1) as PagingLevel),

forall |i: int| {
    level <= i < C::NR_LEVELS()
        ==> (#[trigger] pte_index_spec::<C>(va1, (i + 1) as PagingLevel))
            == pte_index_spec::<C>(va2, (i + 1) as PagingLevel)
},

Addresses in one aligned node select the same entries at that node and above.