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

1

4. q : A/E 5. x : {x:A| q = x }   <x,x> = <q,x>  q:A/E{x:A| q = x  A/E }

2 steps

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