IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
union functionality wrt one one corr113 1. A : Type
2. A' : Type
3. B : Type
4. B' : Type
5. f : AA' 6. g : A'A 7. InvFuns(A;A';f;g)
8. f1 : BB' 9. g1 : B'B 10. InvFuns(B;B';f1;g1)
11. x : A' f(g(x)) = x
By:
BackThru: InvFuns(A;A';f;g)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A'
f(g(x)) = x
