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

B(i)

<a,x/i,b. b> = x

i:{x:A| x = a

A }

B(i)

By:	New:[i \| b] Analyze-1 THEN Reduce Concl

Generated subgoal:

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

About:

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