Function lemma_seq_update_different Copy item path

pub broadcast proof fn lemma_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A)

i1 != i2,

#[trigger] s.update(i2, a)[i1] == s[i1],