Concat

Purpose of exercise

Activities

Requirements

Properties

Notes

The following intrinsic ACL2 functions will be useful in this problem

To state the necessary predicates, it will be helpful to define the following functions