Nuprl - Proof: linorder le neg

(4steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc

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

T:Type, R:(T

Prop).

Linorder(T;x,y.R(x,y))

(

a,b:T.

R(a,b)

strict_part(x,y.R(x,y);b;a))

By:

GenRepD

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. Linorder(T;x,y.R(x,y))
4. a : T
5. b : T
6. R(a,b)
strict_part(x,y.R(x,y);b;a)
2 steps

2 1. T : Type
2. R : TTProp
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)
1 step

About:

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

(4steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc

1	1. T : Type 2. R : TTProp 3. Linorder(T;x,y.R(x,y)) 4. a : T 5. b : T 6. R(a,b) strict_part(x,y.R(x,y);b;a)	2 steps
2	1. T : Type 2. R : TTProp 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)	1 step