PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc find small greater bound extr eq
  (x.Case of x
  (x.Canil  0
  (x.Cau.v, rec:r  InjCase(if u<r inl(*) ; inr(.*) fi; a. r; b. u+1))
  =
  ext{sfa_doc_find_small_greater_bound}
By: Compute
Cox.Case of x
Cox.Canil  0
Cox.Cau.v, rec:r  InjCase(if u<r inl(*) ; inr(.*) fi; a. r; b. u+1)
Co*
Coext{sfa_doc_find_small_greater_bound}

Generated subgoals:

None

About:
listlist_indnatural_number
addlessinlinrdecide
setisectlambdaapplyfunctionequalaxiommarked_clause_thenmarkup_tag
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc