Definitions graph 1 1 Sections Graphs Doc

Some definitions of interest.
nat Def == {i:| 0i }
Thm* Type
le Def AB == B < A
Thm* i,j:. (ij) Prop
not Def A == A False
Thm* A:Prop. (A) Prop
upto Def upto(i;j) == if i < j [i / upto(i+1;j)] else nil fi (recursive)
Thm* i,j:. upto(i;j) {i..j} List

About:
listconsnilifthenelseintnatural_numberaddless_thanset
recursive_def_noticeuniversememberpropimpliesfalseall!abstraction

Definitions graph 1 1 Sections Graphs Doc