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)))
  EquivRel x,y:A. R(x,y)

1	Refl(A;x,y.R(x,y))	2 steps
2	Sym x,y:A. R(x,y)	1 step
3	Trans x,y:A. R(x,y)	4 steps

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