Nuprl - Proof: singleton singleton self 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: singleton singleton self 1 1

1. A : Type
2. a : A
3. a

{a:A}
4. x : {a:A}

{x:{a:A}| x = a }

By:

Analyze

Generated subgoal:

1 x = a
1 step

About:

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