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