Nuprl - Proof: card curry 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card curry 1 1

1. A : Type
2. B : A

Type
3. C : (x:A

B(x))

Type

InvFuns(z:(x:A

B(x))

C(z);x:A

y:B(x)

C(<x,y>)

InvFuns;

e,x,y. e(<x,y>);

e,z. z/x,y. e(x,y))

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

Generated subgoals:

1 4. e : z:(x:AB(x))C(z)
(z.z/x,y. e(<x,y>)) = e
1 step

2 4. e : x:Ay:B(x)C(<x,y>)
(x,y. e(x,y)) = e
1 step

About:

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

1	4. e : z:(x:AB(x))C(z) (z.z/x,y. e(<x,y>)) = e	1 step
2	4. e : x:Ay:B(x)C(<x,y>) (x,y. e(x,y)) = e	1 step