Nuprl - Proof: card pi 1 1

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

1. A : Type
2. A' : Type
3. B : A

Type
4. B' : A'

Type
5. f : A

A'
6. g : A'

A
7. F : x:A

B(x)

B'(f(x))
8. G : x:A

B'(f(x))

B(x)
9. InvFuns(A;A';f;g)
10.

u:A. InvFuns(B(u);B'(f(u));F(u);G(u))

InvFuns(x:A

B(x);x:A'

B'(x)

InvFuns;

x:A'. F(g(x),e(g(x)));

x:A. G(x,e(f(x))))

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

Generated subgoals:

1 11. e : x:AB(x)
12. x : A
G(x,F(g(f(x)),e(g(f(x))))) = e(x)
2 steps

2 11. e : x:A'B'(x)
12. x : A'
F(g(x),G(g(x),e(f(g(x))))) = e(x) B'(x)
2 steps

About:

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

1	11. e : x:AB(x) 12. x : A G(x,F(g(f(x)),e(g(f(x))))) = e(x)	2 steps
2	11. e : x:A'B'(x) 12. x : A' F(g(x),G(g(x),e(f(g(x))))) = e(x) B'(x)	2 steps