pub proof fn lemma_drop_last_contains_different<T>(s: Seq<T>, needle: T)Expand description
requires
s.len() > 0,s.last() != needle,#[trigger] s.drop_last().contains(needle) == s.contains(needle),If the last element of the sequence s is different from needle, then whether the sequence
s contains needle after dropping the last element depends on whether s contains needle
before the drop.