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

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

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))

InvFuns(i:{a:A}

B(i);B(a);

f.f(a);

b,i. b)

By:	Analyze THEN Reduce Concl THEN Rename-1: f

Generated subgoal:

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

About:

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