Function lemma_seq_add_index1_alt Copy item path

pub broadcast proof fn lemma_seq_add_index1_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int)

0 <= i < s1.len(),

(#[trigger] s1.add(s2))[i] == #[trigger] s1[i],