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