Verified concat-concat rule:  concat (concat x)  =  concat (map concat x)