|- ∀h t. HD (h::t) = h

|- ∀h t. TL (h::t) = t

|- (∀l. [] ++ l = l) ∧ ∀l1 l2 h. h::l1 ++ l2 = h::(l1 ++ l2)

|- (∀acc. REV [] acc = acc) ∧ ∀h t acc. REV (h::t) acc = REV t (h::acc)

|- ∀L. REVERSE L = REV L []