Nuprl - Proof: partial sort 2 2 2 1

(10steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: partial sort 2 2 2 1

1. T : Type
2. T List
3. P : T

T

Prop
4.

x,y:T. Dec(P(x,y))
5.

x,y:T.

P(x,y)

P(y,x)
6. Q : T

T

7.

x,y:T. Q(x,y)

P(x,y)
8. L' : T List
9.

i:

(||L'||-1).

Q(L'[i],L'[(i+1)])
10. i :

(||L'||-1)
11.

P(L'[i],L'[(i+1)])

P(L'[i],L'[(i+1)])

By:	SupposeNot

Generated subgoals:

None

About:

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

(10steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc