pub proof fn lemma_concat_associative<A>(s1: Seq<A>, s2: Seq<A>, s3: Seq<A>)
s1.add(s2.add(s3)) =~= s1.add(s2).add(s3),
The concatenation of sequences is associative