Nuprl - Proof: card sum family singleton elim 1 2

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

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)

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

B(i);B(a);

ib.ib/i,b. b;

b.<a,b>)

By:	Analyze THEN Reduce Concl

Generated subgoals:

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

2 5. y : B(a)
y = y
Trivial

About:

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

1	5. x : i:{x:A\| x = a }B(i) <a,x/i,b. b> = x i:{x:A\| x = a A }B(i)	7 steps
2	5. y : B(a) y = y	Trivial