Function vstd::seq_lib::lemma_seq_contains_after_push

source · 
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