Append


THEOREM   

The empty list is a left identity element of append.

xs @ [] = xs

Proof unavailable

THEOREM   

The empty list is a right identity element of append.

[] @ xs = xs

Proof unavailable

THEOREM   

Append is associative.

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

Proof unavailable

Parent topics