IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
listify wf2 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) abac
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html