Nuprl - Proof: equiv rel subtyping

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: equiv rel subtyping

T:Type, R:(T

Type), Q:(T

Prop).

(EquivRel x,y:T. R(x,y))

(EquivRel x,y:{z:T| Q(z) }. R(x,y))

By:	RepUnfolds [`equiv_rel`;`trans`;`sym`;`refl`] 0

Generated subgoals:

1 1. T : Type
2. R : TTType
3. Q : TProp
4. a:T. R(a,a)
5. a,b:T. R(a,b)  R(b,a)
6. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
7. a : {z:T| Q(z) }
  R(a,a)
1 step

2 1. T : Type
2. R : TTType
3. Q : TProp
4. a:T. R(a,a)
5. a,b:T. R(a,b)  R(b,a)
6. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
7. a : {z:T| Q(z) }
8. b : {z:T| Q(z) }
9. R(a,b)
  R(b,a)
1 step

3 1. T : Type
2. R : TTType
3. Q : TProp
4. a:T. R(a,a)
5. a,b:T. R(a,b)  R(b,a)
6. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
7. a : {z:T| Q(z) }
8. b : {z:T| Q(z) }
9. c : {z:T| Q(z) }
10. R(a,b)
11. R(b,c)
  R(a,c)
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 : TTType 3. Q : TProp 4. a:T. R(a,a) 5. a,b:T. R(a,b) R(b,a) 6. a,b,c:T. R(a,b) R(b,c) R(a,c) 7. a : {z:T\| Q(z) } R(a,a)	1 step
2	1. T : Type 2. R : TTType 3. Q : TProp 4. a:T. R(a,a) 5. a,b:T. R(a,b) R(b,a) 6. a,b,c:T. R(a,b) R(b,c) R(a,c) 7. a : {z:T\| Q(z) } 8. b : {z:T\| Q(z) } 9. R(a,b) R(b,a)	1 step
3	1. T : Type 2. R : TTType 3. Q : TProp 4. a:T. R(a,a) 5. a,b:T. R(a,b) R(b,a) 6. a,b,c:T. R(a,b) R(b,c) R(a,c) 7. a : {z:T\| Q(z) } 8. b : {z:T\| Q(z) } 9. c : {z:T\| Q(z) } 10. R(a,b) 11. R(b,c) R(a,c)	1 step