Entry	Value
Package Name	natural-thm
Count	2
Theorems	NO_NAME : !e f. ?!fn. fn _0 = e /\ (!n. fn (SUC n) = f (fn n) n) num_CASES : !m. m = 0 \/ (?n. m = SUC n)

Back to main package page