Nuprl - Proof: fpf-cap-single1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-cap-single1 1

1. A : Type
2. eq : EqDecider(A)
3. x : A
4. Top
5. Top

eqof(eq)(x,x) = true

By:	Analyze 2 THEN Unfold `eqof` 0 THEN Reduce 0 THEN AutoBoolCase (e1(x,x)) THEN Analyze -1

Generated subgoal:

1 2. e1 : AA
3. x,y:A. x = y e1(x,y)
4. x : A
5. Top
6. Top
e1(x,x)
1 step

About:

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