Function vstd::seq_lib::lemma_seq_concat_contains_all_elements

pub proof fn lemma_seq_concat_contains_all_elements<A>(x: Seq<A>, y: Seq<A>, elt: A)

Expand description

ensures

(x + y).contains(elt) <==> x.contains(elt) || y.contains(elt),

The concatenation of two sequences contains only the elements of the two sequences

Function vstd::seq_lib::lemma_seq_concat_contains_all_elementsCopy item path