Nuprl - Proof: card sum family singleton elim 1 2 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. 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 : {x:A| x = a }
6. b : B(i)

<a,b> = <i,b>

i:{x:A| x = a }

B(i)

By:

Analyze5

Generated subgoal:

1 5. i : A
6. i = a
7. b : B(i)
<a,b> = <i,b> i:{x:A| x = a }B(i)
5 steps

About:

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