Nuprl - Proof: all quot elim 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all quot elim 1 2

1. T : Type
2. E : T

Prop
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:T. F(z)
7. z : x,y:T//E(x,y)

F(z)

By:	Unfold `sq_stable` 5 THEN BackThru 5

Generated subgoal:

1 5. w:x,y:T//E(x,y). (F(w)) F(w)
6. z:T. F(z)
7. z : x,y:T//E(x,y)
(F(z))
4 steps

About:

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