Nuprl - Proof: compose iter inverses

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

A:Type, f,g:(A

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

(

. InvFuns(A;A;f{

i};g{

i}))

By:

Analyze

Generated subgoal:

1 1. A : Type
f,g:(AA). InvFuns(A;A;f;g) (i:. InvFuns(A;A;f{i};g{i}))
11 steps

About:

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