Nuprl - Proof: listify wf 2

(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-m

k

(

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:

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

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