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,
)

requires

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

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

ensures

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