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

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

1. A : Type
2. a : A
3. B : {a:A}

Type
4. a

{a:A}
5. (

b,i. b)

B(a)

(i:{a:A}

B(i))
6. f : i:{a:A}

B(i)

(

i.f(a)) = f

By:	FunExtensionality

Generated subgoals:

1 7. x : {a:A}
f(a) = f(x) B(x)
2 steps

2 (i.f(a)) i:{a:A}B(i)
3 steps

About:

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

1	7. x : {a:A} f(a) = f(x) B(x)	2 steps
2	(i.f(a)) i:{a:A}B(i)	3 steps