Function lemma_seq_update_different_alt

pub broadcast proof fn lemma_seq_update_different_alt<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] == #[trigger] s[i1],

lemma_seq_update_different_alt