Function vstd::seq_lib::lemma_seq_contains_after_push

pub proof fn lemma_seq_contains_after_push<A>(s: Seq<A>, v: A, x: A)

Expand description

ensures

(s.push(v).contains(x) <==> v == x || s.contains(x)) && s.push(v).contains(v),

After pushing an element onto a sequence, the sequence contains that element

Function vstd::seq_lib::lemma_seq_contains_after_pushCopy item path