Function lemma_seq_push_index_different Copy item path

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

i < s.len(),

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