as,bs:T List. rev(as @ bs) = (rev(bs) @ rev(as))as:T List. (as @ nil) = asas,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs))| Theorem | Name |
| as,bs:T List. rev(as @ bs) = (rev(bs) @ rev(as)) | [reverse_append] |
| cites the following: | |
| as:T List. (as @ nil) = as | [append_back_nil] |
| as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs)) | [append_assoc] |