A:Type. 
   E:(AAProp) st EquivRel a,a':A. E(a;a'). (q:A/E{x:A| q = x  A/E }) ~ A

1

1. A : Type 2. E : AAProp 3. EquivRel a,a':A. E(a;a')   (q:A/E{x:A| q = x }) ~ A

5 steps

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