Function lemma_seq_update_same_alt Copy item path

pub broadcast proof fn lemma_seq_update_same_alt<A>(s: Seq<A>, i: int, a: A)

0 <= i < s.len(),

s.update(i, a)[i] == a,