WhoCites Definitions MarkB generic Sections NuprlLIB Doc

Who Cites nat?
natDef == {i:| 0i }
Thm* Type
le Def AB == B < A
Thm* i,j:. (ij) Prop
not Def A == A False
Thm* A:Prop. (A) Prop

Syntax: has structure: nat

About:
intnatural_numberless_thansetuniversemember
propimpliesfalseall!abstraction

WhoCites Definitions MarkB generic Sections NuprlLIB Doc