1. A : Type
2. R : AAProp
3. x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z)))
4. a : A
5. b : A
6. c : A
7. R(a,b)
8. R(b,c)
  R(a,c)

1

9. R(a,a) 10. y:A. R(a,y)  R(y,a) & (z:A. R(y,z)  R(a,z))   R(a,c)

2 steps

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