Function lemma_seq_two_subranges_index

pub broadcast proof fn lemma_seq_two_subranges_index<A>(
    s: Seq<A>,
    j: int,
    k1: int,
    k2: int,
    i: int,
)

Expand description

requires

0 <= j <= k1 <= s.len(),

0 <= j <= k2 <= s.len(),

0 <= i < k1 - j,

0 <= i < k2 - j,

ensures

#[trigger] s.subrange(j, k1)[i] == (#[trigger] s.subrange(j, k2))[i],

lemma_seq_two_subranges_index