Function vstd::seq_lib::lemma_flatten_concat
source · pub proof fn lemma_flatten_concat<A>(x: Seq<Seq<A>>, y: Seq<Seq<A>>)Expand description
ensures
(x + y).flatten() =~= x.flatten() + y.flatten(),Flattening sequences of sequences is distributive over concatenation. That is, concatenating the flattening of two sequences of sequences is the same as flattening the concatenation of two sequences of sequences.