The empty list is a left identity element of append.

`xs @ [] = xs`

Proof unavailable

The empty list is a right identity element of append.

`[] @ xs = xs`

Proof unavailable

Append is associative.

`append_assoc: (?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs`

Proof unavailable