Nuprl - Proof: trans imp sp trans

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: trans imp sp trans

T:Type, R:(T

Prop).

(Trans a,b:T. R(a,b))

(Trans a,b:T. strict_part(x,y.R(x,y);a;b))

By:	Unfolds [`trans`;`strict_part`] 0 THEN GenRepD

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
4. a : T
5. b : T
6. c : T
7. R(a,b)
8. R(b,a)
9. R(b,c)
10. R(c,b)
  R(a,c)
1 step

2 1. T : Type
2. R : TTProp
3. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
4. a : T
5. b : T
6. c : T
7. R(a,b)
8. R(b,a)
9. R(b,c)
10. R(c,b)
  R(c,a)
2 steps

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. a,b,c:T. R(a,b) R(b,c) R(a,c) 4. a : T 5. b : T 6. c : T 7. R(a,b) 8. R(b,a) 9. R(b,c) 10. R(c,b) R(a,c)	1 step
2	1. T : Type 2. R : TTProp 3. a,b,c:T. R(a,b) R(b,c) R(a,c) 4. a : T 5. b : T 6. c : T 7. R(a,b) 8. R(b,a) 9. R(b,c) 10. R(c,b) R(c,a)	2 steps