Nuprl - Proof: compose iter inverses 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose iter inverses 1 2

1. A : Type
2.

f,g:(A

A). InvFuns(A;A;f;g)

(

, x:A. g{

i}(f{

i}(x)) = x)
3. f : A

A
4. g : A

A
5. InvFuns(A;A;f;g)
6. i :

InvFuns(A;A;f{

i};g{

i})

By:

Analyze

Generated subgoals:

1 7. x : A
g{i}(f{i}(x)) = x
1 step

2 7. y : A
f{i}(g{i}(y)) = y
2 steps

About:

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

1	7. x : A g{i}(f{i}(x)) = x	1 step
2	7. y : A f{i}(g{i}(y)) = y	2 steps