Entry	Value
Package Name	natural-dest-def
Count	1
Theorems	PRE : !n. PRE (SUC n) = n

Back to main package page