Nuprl - Proof: partial sort 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: partial sort 2 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. Q(x,y)

Q(y,x)

By:	RW (SweepDnC (HypC -4)) 0 THEN RW (SweepDnC (HypC -4)) -1 THEN EasyHyp

Generated subgoal:

1 10. P(x,y)
P(y,x)
1 step

About:

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