pub proof fn lemma_push_contains_same<T>(s: Seq<T>, needle: T)Expand description
ensures
#[trigger] s.push(needle).contains(needle),The result of pushing element needle into the sequence s contains needle.