pub proof fn lemma_push_contains_different<T>(s: Seq<T>, new_elem: T, needle: T)Expand description
requires
new_elem != needle,#[trigger] s.push(new_elem).contains(needle) == s.contains(needle),If element needle is different from new_elem, then whether the sequence s contains needle
after pushing new_elem depends on whether s contains needle before the push.