Nuprl - Proof: card pi 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card pi 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))

f:((x:A

B(x))

(x:A'

B'(x))), g:((x:A'

B'(x))

(x:A

B(x))).

InvFuns(x:A

B(x);x:A'

B'(x);f;g)

By:	Witness: e.x:A'. F(g(x),e(g(x))) \| e.x:A. G(x,e(f(x))) THENA (ApFun: B' to: f(g(x)) = x A' THENA BackThru: Hyp:9)

Generated subgoal:

1 InvFuns(x:AB(x);x:A'B'(x)
InvFuns;e.x:A'. F(g(x),e(g(x)));e.x:A. G(x,e(f(x))))
5 steps

About:

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