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