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.