Entry	Value
Package Name	list-def
Count	2
Theorems	list_INDUCT : !p. p [] /\ (!h t. p t ==> p (CONS h t)) ==> (!l. p l) list_RECURSION : !b f. ?fn. fn [] = b /\ (!h t. fn (CONS h t) = f h t (fn t))

Back to main package page