Definitions graph 1 1 Sections Graphs Doc

Some definitions of interest.
le Def AB == B < A
Thm* i,j:. (ij) 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_numberadd
less_thanrecursive_def_noticememberpropall!abstraction

Definitions graph 1 1 Sections Graphs Doc