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)
9. R(a,a)
10. y:A. R(a,y)  R(y,a) & (z:A. R(y,z)  R(a,z))
  R(a,c)

1

11. R(a,b)  R(b,a) & (z:A. R(b,z)  R(a,z))   R(a,c)

1 step

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