pub broadcast proof fn lemma_seq_contains_after_push<A>(s: Seq<A>, v: A, x: A)Expand description
ensures
#[trigger] s.push(v).contains(x) <==> v == x || s.contains(x),After pushing an element onto a sequence, the sequence contains that element