Entry	Value
Package Name	list-append-def
Count	4
Theorems	CONS_APPEND : !l h t. APPEND (CONS h t) l = CONS h (APPEND t l) NIL_APPEND : !l. APPEND [] l = l concat_cons : !h t. concat (CONS h t) = APPEND h (concat t) concat_nil : concat [] = []

Back to main package page