Nuprl - Proof: card prod family singleton elim 1 1

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

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

Type
4. a

{a:A}

(i:{a:A}

B(i)) ~ B(a)

By:	Witness: f.f(a) THEN Witness: b,i. b with type B(a)(i:{a:A}B(i))

Generated subgoals:

1   (b,i. b)  B(a)(i:{a:A}B(i))
4 steps

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

About:

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

1	(b,i. b) B(a)(i:{a:A}B(i))	4 steps
2	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)	7 steps