Nuprl - Proof: partial sort 2 1 1

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

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

Prop
4.

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

x,y:T.

P(x,y)

P(y,x)
6. Q : T

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

P(x,y)
8. x : T
9. y : T
10.

P(x,y)

P(y,x)

By:	Analyze 0 THEN Analyze -1 THEN EasyHyp

Generated subgoals:

None

About:

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