Def {i..j} == {k:| i  k < j }

is mentioned by

Thm* (f,x. if x=0 1 else xf(x-1) fi)  (k:. (k)(k+1))	[sfa_doc_factbody_polytyping]
Thm* (x.Case of x Thm* (x.Canil  0 Thm* (x.Cau.v, rec:r  InjCase(if u<r inl(*) ; inr(.*) fi; a. r; b. u+1)) Thm* = Thm* ext{sfa_doc_find_small_greater_bound} Thm*  (k:. x:(k List){y:(k+1)| y greater-bounds x })	[sfa_doc_find_small_greater_bound_extr_eq]
Thm* (k,x. k) Thm* = Thm* ext{sfa_doc_find_greater_bound_stupidly} Thm*  k:x:(k List){y:(k+1)| y greater-bounds x }	[sfa_doc_find_greater_bound_stupidly_extr_eq]
Thm* k:x:(k List){y:(k+1)| y greater-bounds x }	[sfa_doc_find_greater_bound_stupidly]
Thm* k:. x:(k List){y:(k+1)| y greater-bounds x }	[sfa_doc_find_small_greater_bound]
Def y greater-bounds x == i:||x||. x[i]<y	[sfa_doc_greater_list_bound]

In prior sections: int 1 bool 1 int 2 list 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html