(8steps total) PrintForm Definitions list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: listify wf 2

1. T : Type
2. k:m,n:n-mk  (f:({m..n}T). f{m..n T List)
  m,n:f:({m..n}T). f{m..n T List


By: UnivCD
THEN
BackThru: Hyp:2 Using:[imax(0;n-m)]
THEN
BackThru: Thm* a,b,c:aimax(b;c ab  ac


Generated subgoals:

None

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

(8steps total) PrintForm Definitions list 1 Sections StandardLIB Doc