Nuprl - Some Definitions

int_upper	`Def {i...} == {j:\| ij}` `Thm* n:. {n...} Type`
int_seg	`Def {i..j} == {k:\| i k < j}` `Thm* m,n:. {m..n} Type`
function_prim	`Def x:AB(x) == PRIMITIVE {Total functions from A: x.b(x) such that b(x) B(x) for x A }`
lelt	`Def i j < k == ij & j < k`
le	`Def AB == B < A` `Thm* i,j:. ij Prop`
not	`Def A == A False` `Thm* (A) Prop`