Function vstd::seq::axiom_seq_add_index2

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