../../Task/Array-concatenation/ACL2