Def y greater-bounds x == i:||x||. x[i]<y

is mentioned by

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* x:( List){y:| y greater-bounds x }	[sfa_doc_find_intlist_great_bound]
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]

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