1. T : Type
2. R : TTProp
3. EquivRel x,y:T. R(x,y)
4. a : T
5. a' : T
6. b : T
7. b' : T
8. R(a,b)
9. R(a',b')
10. R(b,b')
  R(a,a')

1

3. a:T. R(a,a) 4. a,b:T. R(a,b)  R(b,a) 5. a,b,c:T. R(a,b)  R(b,c)  R(a,c) 6. a : T 7. a' : T 8. b : T 9. b' : T 10. R(a,b) 11. R(a',b') 12. R(b,b')   R(a,a')

1 step

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