Function vstd::seq_lib::lemma_concat_associative

source · 
pub proof fn lemma_concat_associative<A>(s1: Seq<A>, s2: Seq<A>, s3: Seq<A>)
Expand description
ensures
s1.add(s2.add(s3)) =~= s1.add(s2).add(s3),

The concatenation of sequences is associative