Nuprl - Proof: card sum family singleton elim 1 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card sum family singleton elim 1 1 1 1 1 1

1. A : Type
2. a : A
3. B : {x:A| x = a }

Type
4. i : A
5. i = a
6. B(i)

i = a

{x:A| x = a }

By:

Analyze

Generated subgoals:

None

About:

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