Function lemma_seq_push_index_different_alt Copy item path

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

0 <= i < s.len(),

(#[trigger] s.push(a))[i] == #[trigger] s[i],