lemma_seq_add_index2_alt

vstd::seq

Function lemma_seq_add_index2_alt 

Source 
pub broadcast proof fn lemma_seq_add_index2_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int)
Expand description
requires
0 <= i < s2.len(),
ensures
(#[trigger] s1.add(s2))[i + s1.len()] == #[trigger] s2[i],