Function vstd::seq_lib::lemma_seq_contains_after_push
source · 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