vstd::seq

Function axiom_seq_update_different

Source 
pub broadcast proof fn axiom_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A)
Expand description
requires
0 <= i1 < s.len(),
0 <= i2 < s.len(),
i1 != i2,
ensures
#[trigger] s.update(i2, a)[i1] == s[i1],