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)

None

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