Entry	Value
Package Name	natural-def
Count	3
Theorems	NO_NAME : !p. p _0 /\ (!n. p n ==> p (SUC n)) ==> (!n. p n) NO_NAME : !n. ~(SUC n = _0) SUC_INJ : !m n. SUC m = SUC n <=> m = n

Back to main package page