IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
all quot elim1 T:Type, E:(TTProp).
(EquivRel x,y:T. E(x,y))
(F:((x,y:T//E(x,y))Prop).
((w:x,y:T//E(x,y). SqStable(F(w)))
( (((z:x,y:T//E(x,y). F(z)) (z:T. F(z))))
1. T : Type
2. E : TTProp
3. EquivRel x,y:T. E(x,y)
4. F : (x,y:T//E(x,y))Prop
5. w:x,y:T//E(x,y). SqStable(F(w))
6. z:x,y:T//E(x,y). F(z)
7. z : T F(z)