Nuprl - Proof: linorder le neg 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: linorder le neg 2

1. T : Type
2. R : T

Prop
3. Linorder(T;x,y.R(x,y))
4. a : T
5. b : T
6. strict_part(x,y.R(x,y);b;a)

R(a,b)

By:	Analyze 6 THEN ProveProp

Generated subgoals:

None

About:

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