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

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

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

Type
4. (

ib.ib/i,b. b)

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

B(i))

B(a)
5. i : A
6. i = a
7. b : B(i)

<a,b> = <i,b>

i:{x:A| x = a }

B(i)

By:

Analyze

Generated subgoals:

1 a = i {x:A| x = a }
1 step

2 b = b B(a)
3 steps

About:

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