pub broadcast proof fn lemma_seq_subrange_index_alt<A>(s: Seq<A>, j: int, k: int, i: int)Expand description
requires
0 <= j <= k <= s.len(),0 <= i - j < k - j,(#[trigger] s.subrange(j, k))[i - j] == #[trigger] s[i],