ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2))as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs)| Theorem | Name |
| ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2)) | [concat_append] |
| cites the following: | |
| as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs) | [append_assoc_sq] |