Function lemma_seq_subrange_composition

pub broadcast proof fn lemma_seq_subrange_composition<A>(
    s: Seq<A>,
    i1: int,
    j1: int,
    i2: int,
    j2: int,
)

Expand description

requires

0 <= i1 <= j1 <= s.len(),

0 <= i2 <= j2 <= j1 - i1,

ensures

#[trigger] s.subrange(i1, j1).subrange(i2, j2) == s.subrange(i1 + i2, i1 + j2),

lemma_seq_subrange_composition